Verification of concurrent code from synchronous specifications - Archive ouverte HAL Access content directly
Journal Articles Science of Computer Programming Year : 2021

Verification of concurrent code from synchronous specifications

(1) , (1, 2) , (3) , (1) , (4)
1
2
3
4

Abstract

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.
Not file

Dates and versions

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

Identifiers

Cite

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⟩
14 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More