-
Chapter and Conference Paper
Formal Verification of an Industrial Distributed Algorithm: An Experience Report
Verification of distributed software is a challenging task. This paper reports on modeling and verification of a consensus algorithm developed by Thales. The algorithm has an arbitrary number of processes (nod...
-
Chapter and Conference Paper
Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking
The election of a leader in a network is a challenging task, especially when the processes are asynchronous, i. e., execute an algorithm with time-varying periods. Thales developed an industrial election algor...
-
Article
DOL-BIP-Critical: a tool chain for rigorous design and implementation of mixed-criticality multi-core systems
Mixed-criticality systems are promoted in industry due to their potential to reduce size, weight, power, and cost. Nonetheless, deploying mixed-criticality applications on commercial multi-core platforms remai...
-
Chapter and Conference Paper
Applying Parametric Model-Checking Techniques for Reusing Real-Time Critical Systems
Due to the increase of complexity in real-time safety-critical systems, verification and validation costs have significantly increased. A straightforward way to reduce costs is to reuse existing systems, adapt...
-
Chapter and Conference Paper
Compositional Analysis of Boolean Networks Using Local Fixed-Point Iterations
We present a compositional method which allows to over-approximate the set of attractors and under-approximate the set of basins of attraction of a Boolean network (BN). This merely consists in replacing a glo...
-
Chapter and Conference Paper
Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed Systems
In this paper, we address the problem of parametric schedulability analysis of distributed real-time systems scheduled by fixed priority. We propose two different approaches to parametric analysis. The first o...
-
Chapter and Conference Paper
Stability Controllers for Sampled Switched Systems
We consider in this paper switched systems, a class of hybrid systems recently used with success in various domains such as automotive industry and power electonics. We propose a state-dependent control strate...
-
Chapter and Conference Paper
Merge and Conquer: State Merging in Parametric Timed Automata
Parameter synthesis for real-time systems aims at synthesizing dense sets of valuations for the timing requirements, guaranteeing a good behavior. A popular formalism for modeling parameterized real-time syste...
-
Chapter and Conference Paper
IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems
The tool Imitator implements the Inverse Method (IM) for Timed Automata (TAs). Given a TA \(\mathcal{A}\) and a tuple π ...
-
Chapter and Conference Paper
Enhancing the Inverse Method with State Merging
Kee** the state space small is essential when verifying real-time systems using Timed Automata (TA). In the model-checker Uppaal, the merging operation has been used extensively in order to reduce the number...
-
Chapter and Conference Paper
Synthesis of Timing Parameters Satisfying Safety Properties
Safety properties are crucial when verifying real-time concurrent systems. When reasoning parametrically, i.e., with unknown constants, it is of high interest to infer a set of parameter valuations consistent ...
