-
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
How to Be Sure a Faulty System Does Not Always Appear Healthy?
Fault diagnosis is a crucial and challenging task in the automatic control of complex systems, whose efficiency depends on the diagnosability property of a system. Diagnosability describes the system property ...
-
Article
Open AccessCompositional schedulability analysis of real-time actor-based systems
We present an extension of the actor model with real-time, including deadlines associated with messages, and explicit application-level scheduling policies, e.g.,“earliest deadline first” which can be associat...
-
Article
Model-based testing for concurrent systems: unfolding-based test selection
Model-based testing has mainly focused on models where concurrency is interpreted as interleaving (like the ioco theory for labeled transition systems), which may be too coarse when one wants concurrency to be pr...
-
Chapter and Conference Paper
Distributed Testing of Concurrent Systems: Vector Clocks to the Rescue
The ioco relation has become a standard in model-based conformance testing. The co-ioco conformance relation is an extension of this relation to concurrent systems specified with true-concurrency models. This rel...
-
Chapter and Conference Paper
Unfolding-Based Test Selection for Concurrent Conformance
Model-based testing has mainly focused on models where currency is interpreted as interleaving (like the ioco theory for labeled transition systems), which may be too coarse when one wants concurrency to be prese...
-
Chapter and Conference Paper
Conformance Relations for Labeled Event Structures
We propose a theoretical framework for testing concurrent systems from true concurrency models like Petri nets or networks of automata. The underlying model of computation of such formalisms are labeled event ...
-
Chapter and Conference Paper
A Specification-Based Test Case Generation Method for UML/OCL
Automated test data generation is an important method for the verification and validation of UML/OCL specifications. In this paper, we present an extension of DNF-based test case generation methods to class mo...
-
Article
Proof-Guided Test Selection from First-Order Specifications with Equality
This paper deals with test case selection from axiomatic specifications whose axioms are quantifier-free first-order formulas with equality. We first prove the existence of an ideal exhaustive test set to star...
-
Article
Some General Results About Proof Normalization
In this paper, we provide a general setting under which results of normalization of proof trees such as, for instance, the logicality result in equational reasoning and the cut-elimination property in sequent ...
-
Chapter and Conference Paper
Integration Testing from Structured First-Order Specifications via Deduction Modulo
Testing from first-order specifications has mainly been studied for flat specifications, that are specifications of a single software module. However, the specifications of large software systems are generally...
-
Chapter and Conference Paper
Specification-Based Testing for CoCasl’s Modal Specifications
Specification-based testing is a particular case of black-box testing, which consists in deriving test cases from an analysis of a formal specification. We present in this paper an extension of the most popula...
-
Chapter and Conference Paper
Test Selection Criteria for Quantifier-Free First-Order Specifications
This paper deals with test case selection from axiomatic specifications whose axioms are quantifier-free first-order formulae. Test cases are modeled as ground formulae and any specification has an exhaustive ...
