Title
Verification Of Concurrent Code From Synchronous Specifications
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. (C) 2021 Elsevier B.V. All rights reserved.
Year
DOI
Venue
2021
10.1016/j.scico.2021.102625
SCIENCE OF COMPUTER PROGRAMMING
Keywords
DocType
Volume
Synchronous specifications, SIGNAL, Parallel programming, OpenMP, Code generation
Journal
206
ISSN
Citations 
PageRank 
0167-6423
0
0.34
References 
Authors
0
5
Name
Order
Citations
PageRank
Kai Hu19012.83
Teng Zhang2163.70
Yi Ding319916.70
Jian Zhu400.68
Jean-Pierre Talpin51163108.42