Hubs for VirtuosoNext: Online verification of real-time coordinators

• Tipo: Artigo em Revista Científica Internacional
• Data: 2021

Autores

Cledou, G (Autor) Outra; Proenca, J (Autor) Outra; Sputh, BHC (Autor) Outra; Verhulst, E (Autor) Outra

Revista

Título: Science of Computer Programming

Vol. 203

ISSN: 0167-6423

Editora: Elsevier

Indexação

ISI Web of Knowledge - 1 Citação

Scopus - 2 Citações

Outras Informações

ID Authenticus: P-00S-ZKJ

DOI: 10.1016/j.scico.2020.102566

Abstract (EN): VirtuosoNextTM is a distributed real-time operating system (RTOS) featuring a generic programming model dubbed Interacting Entities. This paper 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 optimised, 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 definition 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.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 12