PhD proposal (@ ECE Paris/Télécom SudParis).

Context:
=========
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, automatic pilot avionics, etc. The synchronous reactive approaches are widely adopted in the industry and can be definitely used for the software/networking design of complex CPSs.

A system under this approach consists of one or more nodes interacting via an arbitrary network (wired or wireless). Each node is an independent computing entity that handles hardware (processor (CPU), memory, etc) and runs some behavioral tasks. The basic assumption of synchronous languages is based on the following hypothesis: At the moment of an input event, a system node reacts fast enough to produce the output event before the next input event [6]. Based on such hypothesis, the execution of a system node is split into cyclic successive non-overlapping synchronized reactions. A reaction is typically a response after the receipt of some input data streams which are 1) the physical environment sensor data, 2) asynchronous outputs of the other system nodes received asynchronously via network 3) the system outputs at the previous cycles. Figure 1 depicts a simple view about the synchronous approach of system design.

This proposal is around software/networking design orientations of the
project: it is about the definition of a new formal synchronous language
intended to specify, verify and implement the software and network layers of complex 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 powerful strategies. It allows the following functions:
• Contracts consistency verification face to their pre/postconditions and
timing predictions;
• Automatic inference of composite contracts;
• Contracts substitutability and refinement;
• Low-level real-time multi-threaded implementation/code generation;
• Functional/timing specification of networking asynchronous data exchange between the system nodes and the verification of their impact on the system;
• Compliance analysis of networking prototyping/implementation with the timing predictions of the system;

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 components 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
platforms.

References
=============
[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 www.SMT-LIB.org.
[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.
[6] A. Gamati. Designing Embedded Systems with the SIGNAL Programming Language: Synchronous, Reactive Specification. Springer Publishing Company, Incorporated, 1st edition, 2009.

Desired skills and experience
================================
• Minimum qualifications: Master’s degree candidate or engineer in computer sciences;
• 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 (english, french).

Application
=============
• Detailed CV (education, student projects, tools and skills, etc);
• Cover letter (motivations for PhD extension, future projects, etc);
• Marks/Notes of the two previous years;
• Recommendations are appreciated.

Contact
=========
Sebti Mouelhi, Assistant Professor, ECE Paris ([email protected])
Hakima Chaouchi, Full Professor, Télécom SudParis (hakima.chaouchi@telecom-sudparis.eu)