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, 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 functions: • 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 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 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 platforms. 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. 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. Contact ========= Sebti Mouelhi, Assistant Professor, ECE Paris (sebti.moue...@ece.fr<mailto:sebti.moue...@ece.fr>) Hakima Chaouchi, Full Professor, Télécom SudParis (hakima.chaou...@telecom-sudparis.eu<mailto:hakima.chaou...@telecom-sudparis.eu>) -- 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 : sebti.moue...@ece.fr<mailto:sebti.moue...@ece.fr>
_______________________________________________ dev mailing list dev@openstreetmap.org https://lists.openstreetmap.org/listinfo/dev
