TuMult is an Inria International Partner Team between the Kairos team in Inria Sophia Antipolis Méditerranée, FR, and East China Normal University (E.C.N.U.) in Shanghai, CN
Overview
The Kairos team at INRIA (and previously the Oasis and Aoste teams) and the Software Engineering Institute at E.C.N.U. have a long lasting collaboration around models, methods, and tools for safe programming of critical systems, including reactive and/or distributed systems, Cyber Physical Systems (CPS), and Internet of Things (IoT).
Work program for the forthcoming years
- Modeling the Uncertain Environments of Cyber-Physical Systems
Logical Time is one of the main scientific foundation of the Kairos Team. From the background in theory of concurrency, we are used to consider mainly discrete control systems that can guarantee a functional determinism independently of any implementation-specific timing variation. Addressing CPS and IoT means widening those assumptions to consider the external environment as part of the design. The environment obeys the law of physics that usually depend on physical time consideration with models that are approximation of the reality and that necessarily introduce a wide uncertainty on the behavior. This task explores the definition of sound extensions to logical time to capture both the physical continuous behavior and make an abstract characterization as a statistical approximation [FACS’16].
- SMT for Logical Time
While synchronous systems usually focus on finite state-based control systems, our abstraction of logical time relies on both Boolean algebra (for synchronous operations) and integer arithmetic (for synchronizing mechanisms), Solving a system of logical-time constraints is NP-complete but we strive to find efficient algorithms to solve sub-classes of well defined systems. In that context, SMT is a promising solution to combine and solve systems that combine several theories. We had first results on this aspect [SCP’17] but we still need to increase the subset of constraints that can be addressed efficiently as well as the performances of the solving tools.
- Spatio-Temporal Specification for Trustworthy Intelligent Transportation Systems
Focusing on Intelligent Transportation Systems as a subset of CPS, we encounter specific problems. In addition to the temporal factor omni-present in real-time and embedded systems, a physical location plays also a central role. Functions of the system (like a train) must be done both at the right time AND at the right location. This task would focus on extensions of our framework for a spatio-temporal logics based on logical time. This means a description of the location of infrastructures as well as the ability to build constraints that depend both on time (logic or physical) and locations (logical or physical).
- Open pNets
Methods for analyzing and guaranteeing the properties of critical and complex systems, including their data and time depend aspects, have strongly evolved with the emergence of efficient satisfiability checking engines (SAT and SMT). We are working on novel methods combining classical verification paradigms (state-space construction and minimization, model-checking) with SMT approaches to create symbolic and compositional verification methods and tool platforms. We have interesting preliminary results [Forte’16, Avocs’18], and collaborate actively on both fundamental results and prototype development.
