Verification of concurrent code from synchronous specifications - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Science of Computer Programming Année : 2021

Verification of concurrent code from synchronous specifications

Résumé

The synchronous language SIGNAL is a formal specification formalism for developing safety-critical real-time systems. It is a multi-clocked data-flow modeling language suitable for specifying deterministic concurrent behaviors. Its model of computation and communication very well matches recent trends to utilize multi-core processors for executing real-time systems, by taking advantage of its concurrent semantics. The SIGNAL compiler generates code from data-flow specifications while analyzing and verifying safety properties of the system under design: deadlock-freedom, determinism. However, most of recent works have focused on generating sequential code from SIGNAL. Choosing the parallel library OpenMP as the target, this paper proposes a methodology to generate and verify concurrent code automatically from SIGNAL specifications. This is done by first exploring clock relations among signals by application of a so-called clock calculus. Then, specifications are translated into EDGs (Equation-Dependency Graphs) to analyze global data-dependency relations. An EDG is then partitioned into concurrent tasks to help explore parallelism in the original specification while preserving its semantic. Combined with clock relations, parallel tasks are finally mapped onto the OpenMP structures. The proposed approach is illustrated by a realistic case study.
Fichier non déposé

Dates et versions

hal-03487784 , version 1 (17-12-2021)

Identifiants

Citer

Kai Hu, Teng Zhang, Yi Ding, Jian Zhu, Jean-Pierre Talpin. Verification of concurrent code from synchronous specifications. Science of Computer Programming, 2021, 206, pp.1-19. ⟨10.1016/j.scico.2021.102625⟩. ⟨hal-03487784⟩
17 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More