My main research topics concern the specification and verification of temporal properties of concurrent systems.
As regards specification, I am interested in temporal logics and mu-calculi extended with data-handling primitives, which are well-adapted for specifying properties of concurrent systems described using action-based, value-passing formal languages stemming from process algebras.
As regards verification, I am interested in various techniques and algorithms: on-the-fly model checking and equivalence checking, diagnostic generation, partial order reduction, massively parallel verification, ...
- XTL 1.2 (eXecutable Temporal Language) [Mateescu-Garavel-98, Mateescu-98-a] is both a language and a model checker allowing to specify temporal logic properties involving data values and verify them on Labeled Transition Systems (LTSs).
The XTL language provides functional-like primitives for exploring LTSs in various ways. It also allows to handle data values contained in transition labels and to define temporal logic operators as recursive functions computing sets of states and transitions of the LTS.
The XTL model checker was developed using the BCG environment and consists of about 27,000 lines of code (SYNTAX, LOTOS, and C). Data-based extensions of several temporal logics (HML, CTL, ACTL, mu-calculus) were implemented as XTL libraries.
XTL was used for verifying several industrial critical applications:
- Philips' Bounded Retransmission Protocol (BRP)
- Link layer protocol of the IEEE-1394 FireWire serial bus
- Bull's cluster file system
- Invoicing system
- Xpress transfer protocol
- HAVi leader election protocol
- Synchronous hardware
- Hardware/software codesign
- Asynchronous hardware
- Non-refinement transformations of software architectures
- Abstraction and analysis of clinical guidance trees
- Gossiping networks
- Model Checking of Scenario-Aware Dataflow
- Probabilistic Collision Risk Estimation for Autonomous Driving
XTL was also used for building a model checker for the FULL data-based modal logic.
- CAESAR_SOLVE [Mateescu-06-a, Mateescu-03-a] is a generic software library dedicated to the on-the-fly resolution of Boolean Equation Systems (BESs).
The library uses a representation of BESs as boolean graphs, which provide a more intuitive way of reasoning about the dependencies between boolean variables. It currently offers 5 resolution algorithms, based on various exploration strategies of boolean graphs: depth-first search (with variants optimized in memory consumption for acyclic or disjunctive/conjunctive BESs), breadth-first search, etc.
It also provides diagnostics (in the form of boolean subgraphs) explaining the truth value of a given boolean variable [Mateescu-00].
The CAESAR_SOLVE library was developed using the OPEN/CAESAR environment [Garavel-98], and consists of about 16,500 lines of C code.
It is currently used within CADP as verification engine for the EVALUATOR model checker, the BISIMULATOR equivalence checker, and the REDUCTOR tool for on-the-fly reduction of LTSs.
- EVALUATOR 3.6 [Mateescu-06-a, Mateescu-03-a, Mateescu-Sighireanu-03, Mateescu-02, Mateescu-Sighireanu-00] is an on-the-fly model checker for regular alternation-free mu-calculus formulas on LTSs.
This temporal logic is an extension of the alternation-free mu-calculus with ACTL-like action formulas and PDL-like regular formulas, making a good compromise between expressiveness, user-friendliness, and efficiency of model checking algorithms.
The model checker works by translating the verification problem in terms of the on-the-fly resolution of a BES. It is also able to generate diagnostics (portions of the LTS) illustrating the truth value of temporal formulas [Mateescu-00].
EVALUATOR 3.0 was developed jointly with Mihaela Sighireanu using the OPEN/CAESAR environment, and consists of about 10,000 lines of code (SYNTAX/FNC-2 and C).
The version EVALUATOR 3.6 uses the BES resolution algorithms provided by the CAESAR_SOLVE library.
Several libraries of derived temporal operators were also developed, which encode the operators of ACTL and a set of generic property patterns described in ACTL and in regular alternation-free mu-calculus.
EVALUATOR 4.0 [Mateescu-Thivolle-08] is an on-the-fly model checker that evaluates MCL (Model Checking Language) formulas on LTSs.
MCL conservatively extends the regular alternation-free mu-calculus with two kinds of features, indicated below.
- Data-handling constructs: action predicates equipped with data variables and expressions, modalities containing regular expressions with counters over action sequences, parameterized fixed point operators, and data-handling constructs inspired from classical programming languages.
- Fairness constructs: infinite looping and saturation operators generalizing those of PDL-delta, which are able to characterize complex cycles of transitions in the LTS. Although these operators are of alternation depth 2, they can be evaluated in linear-time using the BES resolution algorithm proposed in [Mateescu-Thivolle-08].
The model checker works by translating the verification problem into the resolution of a PBES (Parameterized BES) [Mateescu-98-a,Mateescu-98-b], which is instantiated into a plain BES and solved on-the-fly using the algorithms provided by the CAESAR_SOLVE library.
EVALUATOR 4.0 was developed jointly with Damien Thivolle using the OPEN/CAESAR environment, and consists of about 62,000 lines of code (SYNTAX, LOTOS NT, and C).
EVALUATOR 5.0 [Mateescu-Requeno-18] extends MCL with a probabilistic operator enabling to compute on the fly the probability of a transition sequence, given as a generalized regular formula, in a PTS (Probabilistic Transition System).
EVALUATOR (versions 3.x, 4.0, and 5.0) was used for verifying several industrial critical applications:
EVALUATOR (versions 3.x, 4.0, and 5.0) also serves as a component in other research tools connected to CADP:
- Deriving global properties from local restrictions
- Model checking genetic regulatory networks using GNA and CADP
- Abstract interpretation toolkit for mCRL
- Contracts and protocols for Web services
- ANNOTATOR tool for on-the-fly data flow analysis
- VERCORS platform for model checking distributed components
- LYS knowledge analysis toolset for epistemic verification
- Enhanced version of the CRESS tool: analysis of composed grid services
- ITACA/ACIDE toolbox for composition and adaptation of Web services
- Alvis modelling language for embedded systems
- Argos Tool for Analysing UML Descriptions
- Formal Modeling and Validation of BPEL-based Web Service Composition
- Framework for Model-Checking Dataflow in Service Compositions
- OCARINA Tool for Analysing AADL Descriptions
- LFD-MPI Tool for Lightweight Formal Development of MPI Applications
- Tools and Methods for RTCP-nets Modeling and Verification
- Formal Analysis of Security Guidelines for Program Certification
- Adaptive Service Composition Based on Runtime Verification of Formal Properties
- CLEAR Tool for Summarisation of Model Checking Counterexamples
- Meta-Modeling Tool [εm] for Analysis of Process Models
- Automated Analysis of Workflow Applications
- MOZART Tool for Designing and Deploying Advanced IoT Applications
- SLiVER Tool for Modeling and Analyzing Multi-agent Systems
- Debugging and Verification Tools for LINGUA FRANCA in GEMOC Studio
- Probabilistic Analysis of Industrial IoT Applications
- Probabilistic Model Checking of BPMN Processes at Runtime
- BISIMULATOR [MO-08-a, MO-08-b, Mateescu-06-a, BDJM-05, Mateescu-03-a] is an on-the-fly equivalence checker comparing two LTSs modulo a given equivalence or preorder relation.
The tool currently provides seven equivalence relations and their associated preorders: strong, branching, observational, tau*.a, safety, trace, and weak trace.
BISIMULATOR works by translating the verification problem in terms of the on-the-fly resolution of a BES. It is also able to generate counterexamples (acyclic graphs containing distinguishing sequences) illustrating the non equivalence of two LTSs.
BISIMULATOR was developed using the OPEN/CAESAR environment, and consists of about 23,000 lines of C code.
The tool uses the BES resolution algorithms provided by the CAESAR_SOLVE library.
BISIMULATOR was used for verifying several industrial critical applications:
- Asynchronous network-on-chip
- Registrar entity for the Session Initiation Protocol (SIP)
- Dutch Rijnland Internet Election System (RIES)
- Collaboration diagrams
- Validation of semantic composability in simulation models
- Performance evaluation of MPI on CC-NUMA architectures
- Translation validation of (multi-clocked) SIGNAL specifications
- Scalably Verifiable Cache Coherence
- SYNERGY Reconfiguration Protocol
- Self-configuration Protocol for the Cloud
- Learning and Testing the Bounded Retransmission Protocol
- Assisting Refinement in System-on-Chip Design
- Verification of Plastic User Interfaces Exploiting Domain Ontologies
- Model-Based Diagnosis using LNT
- Finding Conservative Schema Evolutions by Analysing API Changes
- CUNCTATOR [CGH+10] is an on-the-fly steady-state simulator for Continuous-Time Markov Chains (CTMCs).
Taking as input an extended Markovian model, the tool converts it on-the-fly into a CTMC by applying user-given hiding and renaming rules on transition labels, and explores a transition sequence on-the-fly.
Upon termination of the simulation, which occurs when the number of transitions explored or the virtual time reaches a user-given limit, the tool displays the throughputs of specified transitions, together with additional information (number of invisible transitions, presence of nondeterminism, etc.).
The current context of the simulation can be saved and used as starting point for other simulations, which enables an efficient implementation of convergence criteria (e.g., based on confidence intervals) by performing a sequence of increasingly long simulations (each one being the prefix of the subsequent ones) in linear time.
CUNCTATOR was developed using the OPEN/CAESAR environment, and consists of about 6,000 lines of C code.
CUNCTATOR was used by Bull for evaluating the performance of MPI implementations [Zidouni-10].
