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.

In 2024, we have addressed the problem of scalability by using a causality clock graph, which is based on static analysis of the specification to trim the state spacei. This is applied to railway systems TITS 2024.

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. In 2020, in the context of this team we have modeled the uncertain behavior by relying on interval logics instead of deterministic constraints. This work has been published at DATE 2020. Facing uncertain environments, we have to avoid over-specification and allow flexibility in the formal model. To do so, we have proposed to introduce so-called holes inside a CCSL specification. We have used a reinforcement learning algorithm to fill in the holes and produce a full and safe specification. That algorithm relies on witness execution traces (good or bad) that guide the learning towards « safe » specifications as compared to « unsafe » ones. This results was published at RTSS 2021.

Mobility and Spatio-temporal Logics

We have proposed a verification framework for the logic called STEC that extends 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 forms of time, a timeline of foreseeable events at one step, and the physical time line of what actually happens.

Algorihtms for symbolic weak equivalences and Pnets.

Our work was focused on specific theories and algorithms for symbolic and compositional bisimulations (HAL 02406098v1). The result was published
at SMC in Melbourne in October 2021 SMC2021. We have also worked on the Compositional Equivalences Based on Open pNets. This is the visible result of the work initiated with ECNU in 2020 and published in 2022 in Journal of Logical and Algebraic Methods in Programming JLAMP 2022.

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 solvers to reduce the set of rules that are actually fireable and rely on a manual decision from 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.

Later, we made further progress to define a dynamic logics that combines a reactive imperative style to describe programs and a declarative style inspired by CCSL to capture properties to be satisfied. We use SMT solvers to decide which rewriting rules, among those that define the semantics of the reactive program, should be fired to satisfy the properties expressed as constraints. The benefit from classical CCSL is that we only rely on a decidable theory in SMT while the full CCSL language requires logics that are not decidable.

Once the requirements are captured, we still have to be able to verify the correction of the properties. However, the more expressive the language, the more difficult the verification. The considered systems are far beyond the frontier of standard decidable formalism. So we have to mix automatic techniques with some proof assistants in order to extend the expressiveness of the requirements. We have made an interesting contribution under the form of a dynamic logic that combines an operational description of the system (a program) and a set of properties to be verified. Compared to the initial work of 2021, the logic (SDL) is not limited to pure clock-based properties but also support a larger set of safety properties (FCS 2022).

This final contribution is a clock-based extension of temporal logics to have a branching-time logics that uses clocks as exploration paths for properties to be validated FAOC 2024.