Models Modeling of Critical Systems

Contact: Frédéric Boulanger

We are interested in the development of systems that are composed of software in interaction with an environment that includes hardware and human beings. Such systems are considered as critical when a failure has heavy consequences on the hardware or the human beings. In that case, it is mandatory to consider verification methods that prevent defaults, and formal models are a good tools to define these methods in a correct way.

Modeling this kind of systems calls to different paradigms, what leads to hybrid and temporized models, especially for cyber-physical systems that mix an hybrid nature with communications.

Verifying this kind of models requires the joint use of different methods, what implies to combine the semantics of these methods in a sound manner.

The critical nature of these systems dictates constraints on the quality of the development process. That is why we also model these processes in order to certify them, according for instance to standards such as CENELEC 50128, Common Criteria ISO 15408, Do 176c etc. The models of these processes define a specification of the development metadata, and allow us to verify that the development document conforms to the specification of the standard. Each standard defines some types of metadata, that are specified by an ontology.

List of publications

Keywords: Model, System, Control, Verification, Validation, Diagnostic, Cyberphysical/Hybrid/Critical systems, Model-driven engineering, Domain Specific Languages, Semantics of Modeling Languages

Software: Isabelle/DOF, HOL-CyberPhy, ModHel'X, TESL

Table of contents

Modeling of development processes using ontologies
A framework for modeling cyberphysical systems
Complex systems development using domain theories
Modeling human reasoning in logic
Multi-paradigm and multi-scale modeling

Members of the theme

Modeling of Development Processes using Ontologies

Participants : Idir AIT-SADOUNE, Achim BRUCKER (Univ. Exeter), Nicolas Meric (phd), Burkhart WOLFF

According to the approach the result of a development process is an integrated document that details the Analysis, Design, Modeling, Implementation, and Test/Verification steps, we designed the Isabelle/DOF system. Isabelle/DOF is for specifying ontologies for annotating models, terms, proofs, text, code, with metadata. This allows for the continuous and automated checking of the conformance of documents to the theory that specify them, i.e. the consistency between informal text and a formal development process.

Isabelle/DOF is deeply integrated into the Isabelle ecosystem, which provides an incremental preview of the consistency check results. It is part of the Archive of Formal Proofs (AFP) and also available in the developer GIT.

Main publications

Invited Talk ABZ 2023, IFM 2019, and Science of Computer Programming 2024. Poster available

A Cyberphysical System Modeling Framework

Participants: Benoît BALLENGHIEN (phd), Paolo Crisafulli (IRT SystemX), Adrien DURIER, Benjamin PUYOBRO (phd), Burkhart WOLFF

HOL-Cyberphy is a framework for modeling actors as communicating processes that are synchronized at given times on their physical state (position, speed, acceleration) by a daemon. It relies on the HOL-CSP theory in Isabelle/HOL. The model generates traces as series of snapshots, which are usual in the simulators of automotive industrials, and allow for deductive reasoning on the set of all traces.

A use-case of the framework is the modeling of non-deterministic decision algorithms in the actors. These algorithms (driving policies for instance) can be analyzed and their safety can be proven in all generality.

HOL-Cyberphy and different use-cases are available in our developer GIT.

Main publications

Robotics and Autonomous Systems 2023, Poster available

Complex systems development using domain theories

Participants : Idir AIT-SADOUNE

One of the main goals of the ANR EBRP project is the definition of extension mechanisms for the Event-B method rather than domain-specific modelling languages. Extending Event-B to support complex system developments requiring the modelling of complex mathematical objects and the support of associated proofs remains a research challenge. The development approach advocated in the ANR EBRP project is being tested for the case of discrete and continuous behaviours. We aim to define domain theories to manage the development of systems from different engineering domains, such as autonomous systems, and domain ontologies, such as cybersecurity, transportation, medical, semantic web, etc.

Main publications

MEDI2019 MEDI2023 Rodin2024

Modeling human reasoning in logic

Participants : Frédéric BOULANGER, Safouan TAHA

In order to capture human behaviors in the diagnosis, monitoring and simulation of systems, we developed a model of the beliefs of a human agent, along with a formal model of the AGM theory of belief revision. This model allowed us to validate a consistency-based algorithm for diagnosing human errors. This work continues in the IDEFIX ANR project.

Poster (in French)

Publications

PhD thesis of Valentin Fouillard, HAR2023, HSMC2021

Multi-paradigm and multi-scale modeling

Participants : Frédéric BOULANGER, Burkhart WOLFF, Safouan TAHA

Modeling complex systems requires the joint use of several modeling paradigms: continuous dynamics, discrete events, state machines and son on. The study of some properties of the system also calls to the use of several models of the system at different scales or abstraction levels.

The mappings between models that rely on different paradigms, as well as between different models of a given system, have to be well defined so that the result of simulations or analysis are sound. One aspect of these mapping is the temporal correspondance between different models, that can be specified in TESL, a language that we designed for synchronizing the simulation of models in the ModHel'X tool, and for which a formal semantics has been defined in Isabelle/HOL.

This work has been applied in different contextes (simulation of Smart Grids, quantitative simulation of cyber-physical systems), and are now applied to the multi-scale simulation of railroads for their supervision.