The project conducted by Centre de recherche de l’ECE Paris (axis Systèmes 
Intelligents et Communiquants) in collaboration with other institutions 
(Télécom SudParis, Université de Versailles, ...) is around the design, 
development and verification of cyber-physical technologies to improve their 
safety, robustness and resilience. The teams involved in the project, tackle 
research topics going from embedded distributed systems, and 
knowledge/learning-based applications, to software-engineering and real-time in 
system design and networking.

A cyber-physical system (CPS) [5]  is a mechanism that is controlled or 
monitored by computer-based algorithms, tightly integrated with the Internet 
and its users. In CPSs, physical and software components are deeply 
intertwined, each operating on different spatial and temporal scales, 
exhibiting multiple and distinct behavioral modalities, and interacting with 
each other in a myriad of ways that change with context. Examples of CPSs 
include smart grid, autonomous automobile systems, medical monitoring, process 
control systems, robotics systems, and automatic pilot avionics, etc. The 
synchronous reactive design approaches are widely adopted in the industry and 
can be definitely used for the software design of CPSs.

This proposal is around software design orientations of the project, and more 
specifically about synchronous design approaches [4] for embedded software. The 
subject is about the definition of a new formal synchronous language intended 
to specify and verify the software and network layers of CPSs.

SNACCC design language
SNACCC (SyNchronous Abstract Contractual Connected Components) is a language 
expected to model and reuse synchronous parameterizable software/hardware 
components on shelves. A SNACCC component is unit of a third-party composition 
with 1) environment interface dependencies which are input and output data 
streams describing resp. its required and provided data, and 2) a set of fixed 
parameters. These parameters are used for generic design purposes i.e., systems 
in such approaches are designed in terms of generic parameters to be specified 
later for specific deployment environments. It is also a unit of a third party 
encapsulation within composite components themselves defined based on 
sub-components. The language cadence components by logical clocks, and some 
data streams can be assigned to others computed at previous cycles. It also 
allows the explicit specifications of timing predictions.

In addition, a SNACCC component is mainly described by an abstract contractual 
specification supposed to reflect the necessary sufficient of its behavior 
without disclosing implementation details. Many results exist around the notion 
of Design-by-Contracts and inherit from different perspectives. Recently in 
2015, a unified vision of this research topic was proposed in [1,2]. The SNACCC 
language is intended to be based on these recent works.

For sake of originality, we aim to combine both end-system functional and 
timing specifications with network analysis of data exchange determinism in 
SNACCC. This will allow software engineering and networking research 
communities to collaborate together within the same reasoning and development 
framework. The idea is to integrate in SNACCC a formal method to reason on the 
network as a separate component. This component must be able to model the 
network in terms of mathematical objects in order to guarantee a safe 
communication between the software endpoints (embedded in the different remote 
subsystems). For example, one of the objectives is to predict the data 
transmission time (depending on their size, network characteristics such as 
bandwidth and others, etc.) and analyze its impacts on the real-time 
performance of the system. All the elements that can be traced useful for the 
application from the network can be integrated in this component.

In this context, the proof engine of SNACCC is expected to be based on SMT [3] 
solvers enriched by inductive proof strategies. It allows the following 
• Contracts consistency verification face to their pre/postconditions and 
timing predictions;
• Automatic inference of composite contracts;
• Contracts substitutability and refinement;
• Functional specification of networking asynchronous data exchange between the 
system nodes and the verification of their impact on the system;
• Compliance of networking specifications with the timing predictions of the 

Ph.D. project
The work may be conducted by following the steps below:
1) state of the art around synchronous, reactive and real-time systems, their 
design and verification formal methods, and their design and implementation 
platforms (like SCADE Suite for Esterel);
2) state of the art around contract-based design approaches and tools;
3) theoretical study of contracts consistency, composition and refinement at 
the different levels of design (functional semantics, timing, etc);
4) inclusion of new design paradigms related to networking part by 
investigating and understating the network communication characteristics 
(synchronous, asynchronous, determinism, random, delay-
tolerant, etc) and limits;
5) in parallel with steps 3) and 4), specification of the logical foundations 
of the syntax and semantics of SNACCC and the (alpha version) implementation of 
the syntactic, type-checking and semantic analyzers of the language.
6) design of the proof engine (using SMT-based inductive based strategies);
7) application to relevant case studies, and prototyping on real embedded 

Desired skills and experience
• Minimum qualifications: Master’s degree candidate or engineer in computer 
• Additional knowledge topics: formal methods and computer science theory, 
synchronous, reactive and real-time systems, networking, knowledge around 
automotive and/or railway systems standards
is recommended but not required;
• Programming languages: OCaml, Ada, C, and Python for scripting;
• Proven written and verbal communication skills.

[1] A. Benveniste, B. Caillaud, D. Nickovic, R. Passerone, J.-B. Raclet, P. 
Reinkemeier, A. Sangiovanni-Vincentelli, W. Damm, T. Henzinger, and K. Larsen. 
Contracts for Systems Design: Methodology and Application cases. Research 
Report RR-8760, Inria Rennes Bretagne Atlantique ; INRIA, July 2015.
[2] A. Benveniste, B. Caillaud, D. Nickovic, R. Passerone, J.-B. Raclet, P. 
Reinkemeier, A. Sangiovanni-Vincentelli, W. Damm, T. Henzinger, and K. Larsen. 
Contracts for Systems Design: Theory. Research Report RR-8759, Inria Rennes 
Bretagne Atlantique ; INRIA, July 2015.
[3] C. Barrett, P. Fontaine, and C. Tinelli. The SMT-LIB Standard: Version 2.5. 
Technical report, Department of Computer Science, The University of Iowa, 2015. 
Available at
[4] A. Benveniste, P. Caspi, S. A. Edwards, N. Halbwachs, P. Le Guernic, and R. 
D. de Simone. The synchronous languages 12 years later. Proceedings of the 
IEEE, 91(1):64–83, Jan 2003.
[5] S. K. Khaitan and J. D. McCalley. Design techniques and applications of 
cyberphysical systems: A survey. IEEE Systems Journal, 9(2):350–365, June 2015.

Sebti Mouelhi, Assistant Professor, ECE Paris 
Hakima Chaouchi, Full Professor, Télécom SudParis 


Sebti Mouelhi
Assistant Professor
ECE Paris - Ecole d'Ingénieurs
Immeuble POLLUX, 37 Quai de Grenelle, 75015 Paris
Office: P500 | Phone: +33 (0) 1 77 48 70 77
Email :<>
dev mailing list

Reply via email to