Back to Search Start Over

Formalizing Time4sys using parametric timed automata

Authors :
Étienne André
Japanese French Laboratory for Informatics (JFLI)
National Institute of Informatics (NII)-The University of Tokyo (UTokyo)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Laboratoire d'Informatique de Paris-Nord (LIPN)
Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS)
National Institute of Informatics (NII)
This work is supported by the ASTREI project funded by the Paris Île-de-France Region, with the additional support of the ANR national research program PACS (ANR-14-CE28-0002) and ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST.
Dominique Mery
Shengchao Qin
ANR PACS (ANR-14-CE28-0002)
ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST
ASTREI project funded by the Paris Île-de-France Region
ANR-14-CE28-0002,PACS,Analyses paramétrées de systèmes concurrents(2014)
André, Étienne
Appel à projets générique - Analyses paramétrées de systèmes concurrents - - PACS2014 - ANR-14-CE28-0002 - Appel à projets générique - VALID
Source :
13th International Symposium on Theoretical Aspects of Software Engineering (TASE 2019), 13th International Symposium on Theoretical Aspects of Software Engineering (TASE 2019), Jul 2019, Guilin, China, TASE
Publication Year :
2019
Publisher :
HAL CCSD, 2019.

Abstract

Critical real-time systems must be verified to avoid the risk of dramatic consequences in case of failure. Thales developed an open formalism Time4sys to model real-time systems, with expressive features such as periodic or sporadic tasks, task dependencies, distributed systems, etc. However, Time4sys does not natively allow for a formal reasoning. In this work, we present a translation from Time4sys to (parametric) timed automata, so as to allow for a formal verification.<br />Comment: This is the author (and slightly extended) version of the manuscript of the same name published in the proceedings of the 13th International Symposium on Theoretical Aspects of Software Engineering (TASE 2019)

Subjects

Subjects :
FOS: Computer and information sciences
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
Formal Languages and Automata Theory (cs.FL)
Programming language
Computer science
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Computer Science - Formal Languages and Automata Theory
020207 software engineering
02 engineering and technology
computer.software_genre
Formal reasoning
[INFO.INFO-ES] Computer Science [cs]/Embedded Systems
Automaton
Software Engineering (cs.SE)
Computer Science - Software Engineering
Formalism (philosophy of mathematics)
0202 electrical engineering, electronic engineering, information engineering
[INFO.INFO-ES]Computer Science [cs]/Embedded Systems
Formal verification
computer
Parametric statistics

Details

Language :
English
Database :
OpenAIRE
Journal :
13th International Symposium on Theoretical Aspects of Software Engineering (TASE 2019), 13th International Symposium on Theoretical Aspects of Software Engineering (TASE 2019), Jul 2019, Guilin, China, TASE
Accession number :
edsair.doi.dedup.....dc02787205977b89784c3cf318752872

Tools

Authors Abstract Subjects Details