New 2006 Results
Test generation on enumerative and symbolic models
- Symbolic test generation
- From Safety Verification to Safety Testing
Controller Synthesis
- Modular and Decentralized Supervisory Control of Concurrent Discrete Event Systems Using Reduced System Models
- A constructive approach to decentralized supervisory Control problems
- Supervisory Control of Symbolic and hybrid Transition systems
Verification and Abstract Interpretation
- Verification of Communication Protocols using Abstract Interpretation of FIFO queues
Transversal Results
- Determinisation of Symbolic Automata
- Supervision Patterns for the Diagnosis of Discrete Event Systems
- Defining and Reasoning About General Recursive Functions in Type Theory
Test generation on enumerative and symbolic models
Key words: testing, test generation, models, transition systems, symbolic
transition systems.
Symbolic test generation
Participants: Jérémy Dubreil, Camille Constant, Hatem Hamdi, Bertrand Jeannet, Thierry Jéron, Vlad Rusu.
For several years we address the generation of symbolic test cases for
testing the conformance of a black-box implementation with respect to
a specification. More specifically, the problem we consider is the
off-line selection of test cases according to a test purpose, which is
here a set of scenarii of interest that one wants to observe during
test execution.
In [tacas05]
and [dipes],
we extend them in the context of infinite-state symbolic models
(IOSTS), by showing how approximate fixpoint computations can be used
in a conservative way. The same kind of technique is also adapted for
test selection with respect to safety properties and its combination
with verification. When dealing with non-deterministic IOSTS
specifications, off-line test selection involves a determinisation
phase, which is not always feasible for IOSTS. However a
determinisation procedure which terminates for a sub-class of IOSTS
has been identified.
Instead of considering the extension of the finite-state IOLTS model
with variables, one can also consider the extension of the IOLTS model
with recursion, which corresponds to a pushdown system. A preliminary
study was done in 2004 with the master thesis of Liva
Randriamanohisoa. One of the problems still to be solved is the
determinisation of a pushdown system which may be necessary when
testing under partial observation. When pushdown automata are
deterministic however, test selection techniques with test purposes
can be used with some adaptations. This is the object of Camille
Constant's PhD.
This year, we also started some work on testing the conformance of
open networks with their security properties. This is part of Jeremy
Dubreil and Hatem Hamdi's PhDs.
From Safety Verification to Safety Testing
Participants : Camille Constant, Thierry Jéron, Hervé Marchand, Vlad Rusu.
In this work we describe a methodology integrating verification and
conformance testing for the formal validation of reactive systems. A
specification of a system - an extended input-output automaton, which
may be infinite-state - and a set of safety properties (``nothing bad
ever happens'') and possibility properties (``something good may
happen'') are assumed. The properties are first tentatively verified
on the specification using automatic techniques based on approximated
state-space exploration, which are sound, but, as a price to pay for
automation, are not complete for the given class of properties.
Because of this incompleteness and of state-space explosion, the
verification may not succeed in proving or disproving the
properties. However, even if verification did not succeed, the testing
phase can proceed and provide useful information about the
implementation. Test cases are automatically and symbolically
generated from the specification and the properties, and are executed
on a black-box implementation of the system. The test execution may
detect violations of conformance between implementation and
specification; in addition, it may detect violation/satisfaction of
the properties by the implementation and by the specification. In this
sense, testing completes verification. The approach is illustrated on
simple examples and on a Bounded Retransmission
Protocol [I2C].
Controller
Synthesis
Key words: controller synthesis methodology,
Hierarchical models, symbolic methods.
Modular and Decentralized Supervisory Control of Concurrent Discrete Event Systems Using Reduced System Models
Participants: Hervé Marchand.
This year we investigated the supervisor synthesis for concurrent
systems based on reduced system models with the intention of
complexity reduction. It is assumed that the expected behavior
(specification) is given on a subset of the system alphabet, and the
system behavior is reduced to this alphabet. Supervisors are computed
for each reduced subsystem employing a modular decentralized
approach. Depending on the chosen architecture, we provide sufficient
conditions for the consistent implementation of the reduced
supervisors for the original
system [wodes06-1]. This
work has been done in cooperation with Klaus Schmidt and Benoit
Gaudin.
A constructive approach to decentralized supervisory Control problems
Participants: Hervé Marchand.
We plunge decentralized control problems into modular ones to benefit
from the know-how of modular control theory: any decentralized control
problem is associated to a natural modular control problem, which
over-approximates it. Then, we discuss how a solution of the latter
problem delivers a solution of the
former [Ifac-DESD]. This
work has been done in cooperation with Jan Komenda and Sophie
Pinchinat.
Supervisory Control of Symbolic and Hybrid Transition systems
Participants: Tristan Le Gall, Bertrand Jeannet, Hervé Marchand
We here tackled the safety controller synthesis problem for various
models (from finite transition systems to hybrid systems). Within this
framework, we are mainly interested in the synthesis problem for an
intermediate model: the symbolic transition system. Modelization needs
lead us to redefine the concept of controllability by associating it
to guards of transitions instead of events. We then define synthesis
algorithms based on abstract interpretation techniques so that we can
ensure finiteness of the computations. We finally generalize our
methodology to the control of hybrid systems, which gives an unified
framework to the supervisory control problem for several classes of
models [TSI].
Verification and Abstract Interpretation
Verification of Communication Protocols using Abstract Interpretation of FIFO queues
Participants: Bertrand Jeannet, Thierry Jéron, Tristan Le Gall.
The PhD thesis of Tristan Le Gall is concerned by the verification of
asynchronous systems communicating through FIFO channels and its
applications. This year, we addressed the verification of
communication protocols or distributed systems that can be modeled by
Communicating Finite State Machines (CFSMs), i.e. a set of sequential
machines communicating via unbounded FIFO channels. Unlike recent
related works based on acceleration techniques, we propose to apply
the Abstract Interpretation approach to such systems, which consists
in using approximated representations of sets of configurations. We
show that the use of regular languages together with an extrapolation
operator provides a simple and elegant method for the analysis of
CFSMs, which is moreover often as accurate as acceleration
techniques, and in some cases more expressive. Last, when the system
has several queues, our method can be implemented either as an
attribute-independent analysis or as a more precise (but also more
costly) attribute-dependent
analysis [Amast].
Transversal Results
Determinisation of Symbolic Automata
Participants: Thierry Jeron, Hervé Marchand, Vlad Rusu.
We define a symbolic determinisation procedure for a class of
infinite-state systems, which consists of automata extended with
symbolic variables that may be infinite-state. The subclass of
extended automata for which the procedure terminates is characterised
as bounded lookahead extended automata. It corresponds to automata
for which, in any location, the observation of a bounded-length trace
is enough to infer the first transition actually taken. We discuss
applications of the algorithm to the verification, testing, and
diagnosis of infinite-state
systems [C-TCS].
Supervision Patterns for the Diagnosis of Discrete Event Systems
Participants: Thierry Jeron, Hervé Marchand,
In this work, we are interested in the diagnosis of discrete event
systems modeled by finite transition systems. We propose a model of
supervision patterns general enough to capture past occurrences of
particular trajectories of the system. Modeling the diagnosis
objective by supervision patterns allows us to generalize the
properties to be diagnosed and to render them independent of the
description of the system. We first formally define the diagnosis
problem in this context. We then derive techniques for the
construction of a diagnoser and for the verification of the
diagnosability based on standard operations on transition systems. We
show that these techniques are general enough to express and solve in
a unified way a broad class of diagnosis problems found in the
literature, e.g. diagnosing permanent faults, multiple faults, fault
sequences and some problems of intermittent
faults [Wodes06-2]. This
work has been done in cooperation with Marie-Odile Cordier (Dream
project-team) and Sophie Pinchinat (S4 project-team).
Our aim is now to extend these results to infinite state systems as
well as to non permanent patterns, and to apply these techniques to
the automatic generation of passive testers (intruder detection
systems) in order to test on-line whether an implementation respects a
given security policy.
Verifying an ATM Protocol Using a Combination of Formal Techniques
Participants: Vlad Rusu.
In this work, we describe a methodology and a case study in formal
verification. The case study is the SSCOP protocol, a member of the
ATM adaptation layer whose main role is to perform a reliable data
transfer over an unreliable communication medium. The methodology
involves: (1) simulation for initial debugging; (2) partial-order
abstraction that preserves the properties of interest; and (3)
compositional verification of the properties at the abstract level
using the PVS theorem prover. Steps (2) and (3) guarantee that the
properties still hold on the whole (composed, concrete) system. The
value of the approach lies in adapting and integrating several
existing formal techniques into a new verification methodology that is
able to deal with real case studies [Comp-J].
Defining and Reasoning About General Recursive Functions in Type Theory
Participants: Vlad Rusu.
We present a practical tool for defining and proving properties of
recursive functions in the Coq proof assistant. The tool proceeds by
generating from pseudo-code (Coq functions that need not be total nor
terminating) the graph of the intended function as an inductive
relation, and then proves that the relation actually represents a
function, which is by construction the function that we are trying to
define. Then, we generate induction and inversion principles, and a
fixpoint equation for proving other properties of the function. Our
tool builds upon state-of-the-art techniques for defining recursive
functions, and can also be used to generate executable functions from
inductive descriptions of their graph. We illustrate the benefits of
our tool on two case
studies FLOPS.