New 2005 Results
Test generation on enumerative and symbolic models
- Symbolic test generation
- From Safety Verification to Safety Testing
- Conformance Testing and Run-time Verification
Controller Synthesis
- Supervisory Control of Structured Discrete Event Systems
- Supervisory Control of Symbolic and hybrid Transition systems
Verification and Abstract Interpretation
- Abstract Lattices for the Analysis of Systems with Unbounded FIFO Channels
- A Relational Abstraction for Functions
- Flat Acceleration in Symbolic Model Checking
Transversal Results
- Determinisation of Symbolic Automata
- Supervision Patterns for the Diagnosis of Discrete Event Systems
- Extracting a Data Flow Analyser in Constructive Logic
- 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: Camille Constant, Bertrand Jeannet, Thierry Jéron, Vlad Rusu.
We address here 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
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. Because of the interactions that occur between the test
case and the implementation, test execution can be seen as a game
involving two players, in which the test case attempts to satisfy the
test purpose (in addition to its role of detecting conformance
errors).
Efficient solutions to this problem have been proposed in the past in
the context of finite-state models, based on the use of fixpoint
computations. In [jeannet05a],
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. We also formalize a quality criterion for test
cases, and we provide a result relating the quality of a generated
test case to the approximations used in the selection algorithm.
Instead of considering the extension of the finite-state IOLTS model
with variables, as in [jeannet05a],
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
main problems still to be solved is the determinisation of a pushdown
system. This determinisation is a necessary operation for test
generation, but is undecidable. To overcome this problem, we study
context-free grammars in order to find a sub-class of these grammars
that can be translated into a deterministic pushdown system. We are
also working on the combination of IOSTS and pushdown systems, which
gives the full expressiveness of a programming language.
From Safety Verification to Safety Testing
Participants: Camille Constant, Thierry Jéron, Hervé Marchand, Vlad Rusu.
In this work, we present a combination of verification and conformance
testing techniques for the formal validation of reactive systems. A
formal specification of a system, which may be infinite-state, and a
set of safety properties are assumed. Each property is verified on the
specification using automatic techniques based on abstract
interpretation, which are sound, but, as a price to pay for
automation, are not necessarily complete. Next, for each property, a
test case is automatically generated from the specification and the
property, and is executed on a black-box implementation of the system
to detect violations of the property by the implementation and
non-conformances between implementation and specification. If the
verification step did not conclude, the test execution may also detect
violations of the property by the specification [rusu05a]. This work
generalizes our previous works on test selection with test purposes,
allowing selection based on safety properties (while test purposes
describe reachability properties). Moreover generated test cases are
decorated with new verdicts.
We have also extended the combination of verification and conformance
testing techniques by considering more expressive properties, allowing
a better and finer selection of test cases. These properties are
represented by observers with internal actions (the same as the
specification) that are unobservable actions. Unfortunately, compared
to [rusu05a], without any assumption about a mapping between the internal
actions of the specification and the ones of the implementation, we
cannot verify whether the implementation violates these properties or
not (internal actions of the implementation are not
known). Nevertheless, we can still detect non-conformances between the
implementation and the specification and violations of the property by
the specification.
Conformance Testing and Run-time Verification
Participants: Sophie Quinton, Vlad Rusu.
The Master's thesis of Sophie Quinton consisted in comparing and
combining run-time verification and conformance testing
techniques. The basic idea of run-time verification is to execute a
program together with a monitor that checks the validity of some
properties on the program's behaviour; typically, the monitor is
automatically synthesized from logical annotations written in the
program's code. On the other hand, conformance testing consists in
comparing the observable behaviour of a black-box implementation of a
system with respect to that described by an operational specification;
this comparison is typically performed by executing the implementation
in parallel with test cases generated from the specification and test
purposes that may be, e.g., reachability or safety properties. This
produces test verdicts about the conformance between implementation
and specification and about the satisfaction of the properties by the
implementation.
Clearly, there are similarities between the two approaches: for
example, monitors and test cases play the same role of observing the
program's behaviour and checking whether it respects some required
properties. There are also some differences: run-time verification
typically checks one particular implementation, namely, the executable
program obtained by compiling the given (annotated) source code. In
contrast, in conformance testing the implementation is not necessarily
derived from the specification - the only requirement is that both
views of the system have the same interface. Moreover, a test case not
only observes, but may also control the implementation in attempting
to satisfy a given test purpose (reachability property), or to violate
a given safety property.
We have shown that many errors that can be discovered by run-time
verification can be formalised as non-conformances with respect to an
adequately chosen specification.
We also propose a methodology for replacing runtime verification by
conformance testing in situations where runtime verification cannot
work, for example, when not all the code of functions constituting the
program under test is available, but only the annotations for those
functions are available.
Controller
Synthesis
Key words: controller synthesis methodology,
Hierarchical models, symbolic methods.
Supervisory Control of Structured Discrete Event Systems
Participants: Benoit Gaudin, Hervé Marchand.
In many applications (as e.g. manufacturing systems, control-command systems,
protocol networks, etc) and control problems, systems are also often modeled by
several components acting concurrently. We are concerned with the control of a
system where its construction is assumed not to be feasible (due to the state
space explosion resulting from the composition), making the use of classical
supervisory control methodologies impractical. Given a concurrent system and a
safety property, modeled as a language, also called
specification that have to be ensured on this system, we investigated
in [gaudin05c] and [komenda05a] the computation of the
supremal controllable language contained in the expected language. We
do not adopt the decentralized approach. Instead, we have chosen to
use a modular centralized approach and to perform the control on some
approximations of the plant derived from the behavior of each
component. The behavior of these approximations is restricted so that
they respect a new language property for discrete event systems called
partial controllability condition that depends on the safety
property. It is shown that, under some assumptions (the objectives
have to be either locally consistent w.r.t. the plant [gaudin05c] or locally controllable
w.r.t. the plant [komenda05a]),
the intersection of these ``controlled approximations'' corresponds to
the supremal controllable language contained in the specification with
respect to the plant. This computation is performed without building
the whole plant, hence avoiding the state space explosion induced by
the concurrent nature of the plant. It is finally shown that the
class of specifications on which our method can be applied strictly
subsumes that considered in Willner and Heyman in 1991.
Meanwhile, we have also been interested in ensuring safety properties
that are more related to the notion of states rather than to the
notion of trajectories of the system (the mutual exclusion problem for
example). For this class of problem, one of the main issue is the
state avoidance control problem, i.e. the supervisor has to
control the plant so that the controlled plant does not reach a set of
forbidden states. Note that if one wants to used a language-based
approach to encode this problem, as e.g. [gaudin05c],
then the obtained specification may be of the size of the global
system itself. This leads us to develop techniques totally devoted to
the state avoidance control problem. Assuming the system is modeled as
concurrent FSMs, we thus provide algorithms that, based on a
particular decomposition of the set of forbidden configurations, solve
the control problem locally (i.e. on each component without computing
the whole system) and produce a global supervisor ensuring the desired
property [gaudin05a].
We then provide sufficient conditions under which the obtained
controlled system is non-blocking [gaudin05d].
This kind of objectives may be useful to perform dynamic interactions
between different parts of a system. Finally, we apply these results
to the case of Hierarchical Finite State Machines [gaudin05b].
Supervisory Control of Symbolic and hybrid Transition systems
Participants: Tristan Le Gall, Bertrand Jeannet, Hervé Marchand.
This year, we have been interested in solving the safety controller
synthesis problem for various models (from finite transition systems
to hybrid systems). Within this framework, we have been mainly
interested in an intermediate model: symbolic transition systems. Due
to the infiniteness of the alphabet, we have chosen to redefine the
concept of controllability by introducing the notion of dynamic
uncontrollable transitions (the controllability status is carried on
by the symbolic transitions by means of guards, instead of the
events). We focus on safety requirements, modeled by observers
that encode the negation of a safety property. We then defined
synthesis algorithms based on abstract interpretation techniques so
that we can ensure convergence of fixpoint computations in a finite
number of steps [legall05b]. We
finally generalized our methodology to the control of hybrid systems,
which gives an unified framework to the supervisory control problem
for several classes of models [legall05a].
Verification and Abstract Interpretation
Abstract Lattices for the Analysis of Systems with Unbounded FIFO Channels
Participants: Bertrand Jeannet, Thierry Jéron, Tristan Le Gall.
The PhD thesis of Tristan Le Gall holds on the verification of
asynchronous systems communicating through FIFO channels and
applications of it. This year, we tackled the reachability analysis of
finite-state systems communicating through unbounded FIFO channels,
using a finite set of messages [RRanalysisFIFO]. Instead of related works relying
on exact acceleration techniques, that may non terminate, our approach
is based on abstract interpretation. We proposed a set of abstract
lattices based on regular languages for representing sets of possible
configurations of FIFO queues. We first focused on the simple case of
systems with only one queue. We then generalized our results to
systems with several queues, for which we proposed both non-relational
and relational abstract lattices (a relational lattice preserves
relations between contents of different queues, while a non relational
one does not). Our experiments show that our method is generally as
precise as exact methods founded on acceleration techniques, while it
is arguably simpler.
A tool is currently being implemented. Our final goal is to extend to
recursive programs the sophisticated techniques implemented in the tool
NBac for reactive programs.
A Relational Abstraction for Functions
Participants: Bertrand Jeannet.
In [jeannet05b]
we are interested in abstracting sets of functions. Main applications
where one needs to infer properties on functions are interprocedural
analysis, analysis of higher-order programs, and shape analysis, where
one may use functions to associate to memory records their field
contents. In [jeannet05b]
we give an overview of existing methods, which are illustrated with
applications to shape analysis, and we formalize a new family of
relational abstract domains that allows sets of functions to be
abstracted more precisely than with known approaches, while being
still machine-representable.
Flat Acceleration in Symbolic Model Checking
Participants: Jérôme Leroux.
Symbolic model checking provides partially effective verification procedures
that can handle systems with an infinite state space. So-called "acceleration
techniques" enhance the convergence of fixpoint computations by computing the
transitive closure of some transitions. We have developed a new framework for
symbolic model checking with accelerations. We have also proposed new symbolic
algorithms using accelerations to compute reachability sets.
We have shown that flatness appears as a central notion in the
verification of counter automata. A counter automaton is called flat when its
control graph can be ``replaced'', equivalently w.r.t. reachability, by
another one with no nested loops.
From a practical view point, we have proved that flatness is a necessary and
sufficient condition for termination of accelerated symbolic model checking, a
generic semi-algorithmic technique implemented in successful tools like
Fast, Lash or TReX.
From a theoretical view point, we have also proved that many known semilinear
subclasses of counter automata are flat: reversal bounded counter machines,
lossy vector addition systems with states, reversible Petri nets, persistent
and conflict-free Petri nets, etc. Hence, for these subclasses, the semilinear
reachability set can be computed using a uniform accelerated symbolic
procedure (whereas previous algorithms were specifically designed for each
subclass) [leroux05a], [leroux05b], [leroux05d], [leroux05c].
Transversal Results
Determinisation of Symbolic Automata
Participants: Thierry Jeron, Hervé Marchand, Vlad Rusu.
Determinisation of symbolic transition systems is a crucial problem
for the verification of properties on external traces, test
generation, and diagnosis based on these models. However STSs cannot
be determinised in general. In this work, we define a symbolic
determinisation procedure for a class of STS. The class consists of
extended automata operating on symbolic variables and synchronizing
with the environment (a simplified version of STS). The subclass of
extended automata for which the procedure terminates is
characterized. This class named ``Bounded Lookahead Automata''
corresponds to systems where non-deterministic choices can be find out
after the observation of a bounded number of actions. Decidable
sufficient conditions for checking termination are also given. This
work is under submission.
Supervision Patterns for the Diagnosis of Discrete Event Systems
Participants: Thierry Jeron, Hervé Marchand,
In this work, we are interested in the diagnosis of finite transition
systems. We propose a model of supervision patterns corresponding to
reachability properties (i.e. violation of a safety property). This
allows to generalize the properties to be diagnosed and to render them
independent of the description of the system. We thus deduce
techniques for the verification of diagnosability and the construction
of a diagnoser 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 [rfia2006l]. 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 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.
Extracting a Data Flow Analyser in Constructive Logic
Participants: Vlad Rusu.
This work has been done in cooperation with David Cachera, Thomas
Jensen, and David Pichardie from the Lande project-team of Irisa. A
constraint-based data flow analysis is formalized in the specification
language of the Coq proof assistant. This involves defining a
dependent type of lattices together with a library of lattice functors
for modular construction of complex abstract domains. Constraints are
represented in a way that allows for both efficient constraint
resolution and correctness proof of the analysis with respect to an
operational semantics. The proof of existence of a solution to the
constraints is constructive which means that the extraction mechanism
of Coq provides a provably correct data flow analyser in Ocaml from
the proof. The library of lattices and the representation of
constraints are defined in an analysis-independent fashion that
provides a basis for a generic framework for proving and extracting
static analysers in Coq [cachera05a].
Defining and Reasoning About General Recursive Functions in Type Theory
Participants: Vlad Rusu.
This is common work with David Pichardie, formerly in the Lande project of Irisa, currently in the Everest project-team at Sophia Antipolis.
In [pichardie05a)] we describe practical method for defining and proving properties of general (i.e., not necessarily structural) recursive functions in proof assistants based on type theory. The idea is to define the graph of the intended function as an inductive relation, and to prove that the relation actually represents a function, which is by construction the function that we are trying to define. Then, we generate induction principles for proving other properties of the function.
The approach has been experimented in the Coq proof assistant, but should work in like-minded proof assistants as well. It allows for functions with mutual recursive calls, nested recursive calls, and works also for the standard encoding of partial functions using total functions over a dependent type that restricts the original function's domain.
We present simple examples and report on a larger case study (sets of integers represented as ordered lists of intervals) that we have conducted in the context of certified static analyses [cachera05a].
In ongoing independent work, yet unpublished, Barthe and Forest from the Everest project at Inria Sophia Antipolis are developing an approach for synthesizing a recursive function from an arbitrary inductive relation. We have submitted a paper to FLOPS'06 (Int. Symposium on Functional and Logic Programming) on a general framework that encompasses both our approaches, as well as on an implementation of these techniques in a prototype tool within Coq.