Repository logo
 
Publication

Hubs for VirtuosoNext: Online verification of real-time coordinators

2021-03-01Journal article Restricted access
Simple item page
dc.contributor.authorCledou, Guillermina
dc.contributor.authorProenca, Jose
dc.contributor.authorSputh, Bernhard H.C.
dc.contributor.authorVerhulst, Eric
dc.date.accessioned2020-12-11T15:18:20Z
dc.date.embargo2120
dc.date.issued2021-03-01
dc.description.abstractVirtuosoNext is a distributed real-time operating system (RTOS) fea- turing a generic programming model dubbed Interacting Entities. This pa- per focuses on these interactions, implemented as so-called Hubs. Hubs act as synchronisation and communication mechanisms between the application tasks and implement the services provided by the kernel. While the kernel provides the most basic services, each carefully designed, tested and opti- mised, tasks are limited to this handful of basic hubs, leaving the development of more complex mechanisms up to application specific implementations. This work presents a toolset that supports the building of new services compositionally, using notions borrowed from the Reo coordination language, on which the developer can delegate coordination-related duties. This toolset uses a formal compositional semantics for hubs that captures dataflow and time, formalising the behaviour of existing hubs, and allowing the defini- tion of new ones. Furthermore, it enables the analysis and verification of hubs under our automata interpretation, including time-sensitive behaviour via the Uppaal model checker, usable on http://arcatools.org/hubs. We illustrate the proposed tools and methods by verifying key properties on different interaction scenarios between tasks and a composed hub.pt_PT
dc.description.versioninfo:eu-repo/semantics/publishedVersionpt_PT
dc.identifier.doi10.1016/j.scico.2020.102566pt_PT
dc.identifier.issn0167-6423
dc.identifier.urihttp://hdl.handle.net/10400.22/16553
dc.language.isoengpt_PT
dc.peerreviewedyespt_PT
dc.publisherElsevierpt_PT
dc.relationPreFECT, ref. POCI-01-0145-FEDER-029119pt_PT
dc.relationRobust and Efficient Approaches to Evaluating Side Channel and Fault Attack Resilience
dc.relationVerification and Validation of Automated Systems' Safety and Security
dc.relation.publisherversionhttps://www.sciencedirect.com/science/article/pii/S016764232030174X?via%3Dihubpt_PT
dc.subjectCoordinationpt_PT
dc.subjectUppaalpt_PT
dc.subjectReal-time OSpt_PT
dc.subjectCompositional semanticspt_PT
dc.titleHubs for VirtuosoNext: Online verification of real-time coordinatorspt_PT
dc.typejournal article
dspace.entity.typePublication
oaire.awardTitleRobust and Efficient Approaches to Evaluating Side Channel and Fault Attack Resilience
oaire.awardTitleVerification and Validation of Automated Systems' Safety and Security
oaire.awardURIinfo:eu-repo/grantAgreement/EC/H2020/731591/EU
oaire.awardURIinfo:eu-repo/grantAgreement/EC/H2020/876852/EU
oaire.citation.issue102566pt_PT
oaire.citation.titleScience of Computer Programmingpt_PT
oaire.citation.volume203pt_PT
oaire.fundingStreamH2020
oaire.fundingStreamH2020
person.familyNameProenca
person.givenNameJose
person.identifier.ciencia-id2412-FE81-2767
person.identifier.orcid0000-0003-0971-8919
person.identifier.ridK-4256-2016
person.identifier.scopus-author-id24067286500
project.funder.identifierhttp://doi.org/10.13039/501100008530
project.funder.identifierhttp://doi.org/10.13039/501100008530
project.funder.nameEuropean Commission
project.funder.nameEuropean Commission
rcaap.rightsclosedAccesspt_PT
rcaap.typearticlept_PT
relation.isAuthorOfPublicationa9b67049-85ec-485a-a937-334ba113f087
relation.isAuthorOfPublication.latestForDiscoverya9b67049-85ec-485a-a937-334ba113f087
relation.isProjectOfPublication49751611-9e4f-4733-a8e5-c7a7d355f16a
relation.isProjectOfPublication1b3082bd-64c8-41d8-9f32-bb7f4b0d7bde
relation.isProjectOfPublication.latestForDiscovery49751611-9e4f-4733-a8e5-c7a7d355f16a

Files

Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
ART_CISTER_2021.pdf
Size:
1.08 MB
Format:
Adobe Portable Document Format
Download

Collections

ISEP – CISTER – Artigos