Location: Inria Sophia Antipolis, Kairos team

Laboratory:

• Laboratoire i3S, UMR 7271
• Laboratoire Méthodes Formelles, UMR 9021, pôle Modélisation des systèmes Critiques,

Duration: 3 years

Context

In the ANR Project #TAPAS, we consider safety-critical systems that have strong interactions with humans and physical components in the domains of electric/autonomous vehicles (EV/AV), (smart) transportation systems (train, tramway), avionics, and healthcare. Such systems must be trustworthy and therefore require sound and formal design frameworks that come with tools for validation and verification. These systems usually exhibits heterogeneous intertwined requirements both functional and non-functional like safety, security, performance, where time plays a key role. These systems usually rely on embedded equipment that are reactive and deterministic, leaving nondeterminism outside their scope of interest. #TAPAS ultimate objective is to define a sound methodology for the design of trustworthy cyber-physical systems (CPS) from requirements to code deployment, supported by an open-source modeling, validation and verification framework. This shall be achieved by plugging into a formal generic language (Event-B) some efficient analysis tools (Provers, Model-checkers, Simulation). We focus on functional and time requirements that are the ground requirements on which systems are built. Indeed, most other considered non functional requirements (safety, security, energy) directly depend on time, more precisely on heterogeneous models of time, including discrete and continuous time.