This team is a collaboration between Kairos Team-Project and East China Normal University in Shanghai. The team has been initiated in 2020 but due to the sanitary conditions, it was started again in January 2022. Unfortunately, no travel was possible in 2022. Travels resumed at the very end of 2023.

A summary paper was published as an LNCS chapter to highlight the main results in the collaboration between Kairos and ECNU (LNCS 2023).

Formal Requirements for Safety-Critical Systems

One of the main issue for building formal requirements is to go from arguably ambiguous English sentences to a precise mathematical notation. Indeed, the English may have a variety of interpretations, which can be good early in the design process, but which makes it difficult to assign a single formal interpretation. To help requirement engineers, we have proposed a technique that uses reinforcement learning to learn from valid scenarios and deduce an actual fitting specification (RTSS 2021). An extension has been published it TCAD 2023. In TC 2023 we show how to accelerate the process by using curiosity-driven exploration.

We are also trying to find informal notations to help express the requirements. In SCP 2022 we show how to rely on UML sequence diagrams to capture those requirements and we have developed a way to verify that they capture the initial intention.

Uncertain environments

CPS are uncertain environments, there are several ways to deal with uncertainty. In the past, we have used stochastic models to characterize the uncertainty. This year, in the context of this team we model the uncertain behavior by relying on interval logics instead of deterministic constraints. This work has been published at DATE 2020.

Mobility and Spatio-temporal Logics

We have proposed a verification framework for the logic called STEC that extend the notion of logical time to space. There was a publication with Zhang Yuanrui (FCS 2020) and Liu Qian (Apsec 2020, Emsoft 2020) has proposed an extension dedicated to the description of safety properties for autonomous vehicles. The logic relies on simple operators that transform observations on the spatial objects of arbitrary shape into logical events. It also combines two form of time, a timeline of foreseeable events at one step, and the physical time line of what actually happens.

Pnets

Our work was focused on specific theories and algorithms for symbolic and compositional bismulations. We had one master thesis, one conference paper published (HAL 02406098v1). An important result started with Chinese students has been published in 2022 (JLAMP 2022) despite the difficulties to attract more students. More of the results are under review.

SMT For Logical Time

We have proposed a dynamic logic (CDL) that relies on a subset of CCSL for the logic and on a synchronous language inspired from Esterel for the program (SCP 2021). The operational semantics of the program is given as rewriting rules but choosing which rule should be fired is undecidable when the language used is Turing-Complete but we use SMT solver to reduce the set of rules that are actually fireable and rely on a manual decision fom the user to finally pick the rule that can be used. In that context, the properties can be encoded with a theory that is decidable (just relying on Presburger arithmetics) and the SMT solver gives us an efficient way to decide.

In 2022, we have proposed an extension (SDL) that can express a wide class of safety properties, beyond pure CCSL (FCS 2022).