Towards a verified compiler prototype for the synchronous language SIGNAL

SIGNAL belongs to the synchronous languages family which are widely used in the design of safety-critical real-time systems such as avionics, space systems, and nu- clear power plants. This paper reports a compiler prototype for SIGNAL. Compared with the existing SIGNAL com- piler, we propose a new intermediate representation （named S-CGA, a variant of clocked guarded actions）, to integrate more synchronous programs into our compiler prototype in the future. The front-end of the compiler, i.e., the transla- tion from SIGNAL to S-CGA, is presented. As well, the proof of semantics preservation is mechanized in the theo- rem prover Coq. Moreover, we present the back-end of the compiler, including sequential code generation and multi- threaded code generation with time-predictable properties. With the rising importance of multi-core processors in safety- critical embedded systems or cyber-physical systems （CPS）, there is a growing need for model-driven generation of multi- threaded code and thus mapping on multi-core. We propose a time-predictable multi-core architecture model in archi- tecture analysis and design language （AADL）, and map the multi-threaded code to this model.

Methods for behavior descriptions of structure-complex Petri nets

Petri net language is a powerful tool for describing dynamic behaviors of physical systems. However, it is not easy to obtain the language expression for a given Petri net especially a structure-complex net. In this paper, we first analyze the behaviors of S-nets, which are structure-simple. With the decomposition method based on a given index function on the place set, a given structure-complex Petri net can be decomposed into a set of structure-simple S-nets. With the language relationships between the original system and the decomposed subnets, an algorithm to obtain the language expression of a given structure-complex net system is presented, which benefits the analysis of physical systems based on the Petri net language.

A comparative study of two formal semantics of the SIGNAL language

SIGNAL is a part of the synchronous languages family, which are broadly used in the design of safety-critical real-time systems such as avionics, space systems, and nu- clear power plants. There exist several semantics for SIG- NAL, such as denotational semantics based on traces （called trace semantics）, denotational semantics based on tags （called tagged model semantics）, operational semantics presented by structural style through an inductive definition of the set of possible transitions, operational semantics defined by syn- chronous transition systems （STS）, etc. However, there is lit- tle research about the equivalence between these semantics. In this work, we would like to prove the equivalence be- tween the trace semantics and the tagged model semantics, to get a determined and precise semantics of the SIGNAL language. These two semantics have several different defini- tions respectively, we select appropriate ones and mechanize them in the Coq platform, the Coq expressions of the abstract syntax of SIGNAL and the two semantics domains, i.e., the trace model and the tagged model, are also given. The dis- tance between these two semantics discourages a direct proof of equivalence. Instead, we transform them to an intermediate model, which mixes the features of both the trace semantics and the tagged model semantics. Finally, we get a determined and precise semantics of SIGNAL.

Multi-threaded code generation from Signal program to OpenMP

The use of multi-core processors will become a trend in safety critical systems. For safe execution of multi- threaded code, automatic code generation from formal spec- ification is a desirable method. Signal, a synchronous lan- guage dedicated for the functional description of safety crit- ical systems, provides soundness semantics for determinis- tic concurrency. Although sequential code generation of Sig- nal has been implemented in Polychrony compiler, deter- ministic multi-threaded code generation strategy is still far from mature. Moreover, existing code generation methods use certain multi-thread library, which limits the cross plat- form executions. OpenMP is an application program inter- face （API） standard for parallel programming, supported by several mainstream compilers from different platforms. This paper presents a methodology translating Signal program to OpenMP-based multi-threaded C code. First, the intermedi- ate representation of the core syntax of Signal using syn- chronous guarded actions is defined. Then, according to the compositional semantics of Signal equations, the Signal pro- gram is synthesized to dependency graph （DG）. After par- allel tasks are extracted from dependency graph, the Signal program can be finally translated into OpenMP-based C code which can be executed on multiple platforms.

On the use of formal methods to model and verify neuronal archetypes

Having a formal model of neural networks can greatly help in understanding and verifying their properties,behavior,and response to external factors such as disease and medicine.In this paper,we adopt a formal model to represent neurons,some neuronal graphs,and their composition.Some specific neuronal graphs are known for having biologically relevant structures and behaviors and we call them archetypes.These archetypes are supposed to be the basis of typical instances of neuronal information processing.In this paper we study six fundamental archetypes(simple series,series with multiple outputs,parallel composition,negative loop,inhibition of a behavior,and contralateral inhibition),and we consider two ways to couple two archetypes:(i)connecting the output(s)of the first archetype to the input(s)of the second archetype and(ii)nesting the first archetype within the second one.We report and compare two key approaches to the formal modeling and verification of the proposed neuronal archetypes and some selected couplings.The first approach exploits the synchronous programming language Lustre to encode archetypes and their couplings,and to express properties concerning their dynamic behavior.These properties are verified thanks to the use of model checkers.The second approach relies on a theorem prover,the Coq Proof Assistant,to prove dynamic properties of neurons and archetypes.