@article{BCHL-jour,
address = {Brisbane, Australia},
author = {Bertrand, N. and Charon, I. and Hudry, O. and
Lobstein, A.},
journal = {Australasian Journal of Combinatorics},
month = fevrier,
ra = false,
pages = {21-35},
publisher = {University of Queensland},
title = {1-Identifying Codes on Trees},
volume = 31,
year = 2005
}
@article{ABRS-lossy,
author = {Abdulla, P.A. and Bertrand, N. and Rabinovich,
A. and Schnoebelen, Ph.},
DOI = {10.1016/j.ic.2005.05.008},
journal = {Information and Computation},
month = novembre,
number = 2,
ra = false,
pages = {141-165},
publisher = {Elsevier Science Publishers},
title = {Verification of Probabilistic Systems with Faulty
Communication},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-ABRS.pdf},
volume = 202,
year = 2005,
abstract = {Many protocols are designed to operate correctly
even in the case where the underlying communication
medium is faulty. To capture the behavior of such
protocols, Lossy Channel Systems (LCS's) have been
proposed. In an LCS the communication channels are
modeled as unbounded FIFO buffers which are
unreliable in the sense that they can
nondeterministically lose messages. Recently,
several attempts have been made to study
Probabilistic Lossy Channel Systems (PLCS's) in
which the probability of losing messages is taken
into account. In this article, we consider a variant
of PLCS's which is more realistic than those studied
previously. More precisely, we assume that during
each step in the execution of the system, each
message may be lost with a certain predefined
probability. We show that for such systems the
following model-checking problem is decidable: to
verify whether a linear-time property definable by a
finite-state omega-automaton holds with probability
one. We also consider other types of faulty
behavior, such as corruption and duplication of
messages, and insertion of new messages, and show
that the decidability results extend to these
models. }
}
@TECHREPORT{RRanalysisFIFO,
AUTHOR = {Jeannet, Bertrand and Jéron, Thierry and Le Gall,
Tristan},
TITLE = {Abstract lattices for the analysis of systems with
unbounded {FIFO} channels},
INSTITUTION = {IRISA},
YEAR = 2005,
NUMBER = 1767,
MONTH = decembre,
abstract = {We address the analysis and the verification of
communicating systems, which are systems built from
sequential processes communicating via unbounded
FIFO channels. We adopt the Abstract Interpretation
approach to this problem, by defining approximate
representations of sets of configuration of FIFO
channels. In this paper we restrict our attention to
the case where processes are finite-state processes
and the alphabet of exchanged messages is finite. We
first focus on systems with only one queue, for
which we propose an abstract lattice based on
regular languages, and we then generalize our
proposal to systems with several queues. In
particular, we define for these systems two abstract
lattices, which are resp. non-relational and
relational abstract lattices. We use those lattices
for computing an over-approximation of the
reachability set of a CFSM. Our experimental
evaluation shows that, for some protocols, we obtain
results that are as good as those obtained by exact
methods founded on acceleration techniques. },
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/PI-1767.ps},
note = {also INRIA report No 5784}
}
@Misc{a,
}
@ARTICLE{cachera05a,
AUTHOR = {Cachera, D. and Jensen, T. and Pichardie, D. and
Rusu, V.},
TITLE = {Extracting a data flow analyser in constructive
logic},
JOURNAL = {Theoretical Computer Science},
YEAR = 2005,
VOLUME = 342,
NUMBER = 1,
doi = {http://dx.doi.org/10.1016/j.tcs.2005.06.004},
PAGES = {56--78},
MONTH = septembre,
ABSTRACT = {A constraint-based data flow analysis is formalised
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. },
pdf = http://www.irisa.fr/vertecs/Publis/Ps/2005-TCS.pdf
}
}
@INPROCEEDINGS{gaudin05a,
AUTHOR = {Gaudin, B. and Marchand, H.},
TITLE = {Efficient Computation of supervisors for loosely
synchronous Discrete Event Systems: A State-Based
Approach},
BOOKTITLE = {6th IFAC World Congress},
YEAR = 2005,
ADDRESS = {Prague, Czech Republic},
MONTH = juillet,
ABSTRACT = {In this paper, we are interested in the control of a
particular class of Concurrent Discrete Event
Systems defined by a collection of components that
interact with each other. We here consider the state
avoidance control problem. We provide algorithms
that, based on a particular decomposition of the set
of forbidden states, locally solve the control
problem (i.e. on each component without computing
the whole system) and produce a global supervisor,
that can be efficiently evaluated on the fly.},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2005-ifac.pdf}
}
@INPROCEEDINGS{gaudin05b,
AUTHOR = {Gaudin, B. and Marchand, H.},
TITLE = {Safety Control of Hierarchical Synchronous Discrete
Event Systems: A State-Based Approach},
BOOKTITLE = {13th Mediterranean Conference on Control and
Automation},
YEAR = 2005,
ADDRESS = {Limassol, Cyprus},
MONTH = juin,
PAGES = {889-895},
ABSTRACT = {In this paper, we discuss the control of a
particular class of Hierarchical Discrete Event
Systems and the state avoidance control problem is
considered. A methodology is provided that locally
computes on each component of the system the set of
bad states (these are the states that may lead to
the forbidden states via an uncontrollable
trajectory). This is performed without computing
the whole system. At this point, the supervisor is
evaluated on the fly w.r.t. the bad states and thus
requires an on-line evaluation in order to determine
the set of events that has to be disabled by
control. It is performed in such a way that the
global partial transition function does not need to
be built.},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2005_med.pdf}
}
@INPROCEEDINGS{gaudin05c,
AUTHOR = {Gaudin, B. and Marchand, H.},
TITLE = {Une approche modulaire pour le contrôle de systèmes
à événements discrets concurrents},
BOOKTITLE = {5ième Colloque Francophone sur la Modélisation des
Systèmes Réactifs (MSR'05)},
YEAR = 2005,
ADDRESS = {Grenoble (Autrans), France},
MONTH = octobre,
CONFNAT = true,
ABSTRACT = {Dans cet article, nous nous intéressons au contrôle
de systèmes à événements discrets concurrents
définis par une collection de sous-systèmes
interagissant les uns avec les autres. Étant donné
un objectif de contrôle, le but consiste à calculer
un superviseur maximal assurant cet objectif, sans
construire explicitement le système à contrôler.
Des approximations du système G sont dérivés à
partir des sous-systèmes qui le composent, et une
propriété appelée contrôlabilité partielle, devant
être vérifiée par l'objectif sur ces approximations,
est introduite. Assurer la contrôlabilité partielle
de l'objectif sur chacune des approximations permet,
sous certaines hypothèses, d'en déduire un
superviseur maximal assurant l'objectif de contrôle
sur G. Les calculs effectués ont une faible
complexité et ne nécessitent pas de construire
explicitement le système G, évitant ainsi
l'explosion combinatoire inhérente aux systèmes
concurrents.},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2005-MSR-Syst-Concur.pdf}
}
@INPROCEEDINGS{gaudin05d,
AUTHOR = {Gaudin, B. and Marchand, H.},
TITLE = {Supervisory Control and Deadlock Avoidance Control
Problem for Concurrent Discrete Event Systems},
BOOKTITLE = {44nd IEEE Conference on Decision and Control
(CDC'05) and Control and European Control Conference
ECC 2005},
PAGES = {2763-2768},
YEAR = 2005,
ADDRESS = {Seville (Spain)},
MONTH = decembre,
ABSTRACT = {In this paper, we tackle the Supervisory Control
Problem control for Concurrent Discrete Event
Systems. These are systems that are defined by a
collection of components that interact with each
other. In this study, we first outline the method
allowing to solve the state avoidance control
problem on concurrent system, without having to
compute the whole system. We then present results
offering an efficient method to detect deadlock
states in the controlled system due either to the
composition or to the control that is performed on
the system.},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2005-CDC-Blocking.pdf}
}
@INPROCEEDINGS{jeannet05a,
AUTHOR = {Jeannet, B. and Jéron, T. and Rusu, V. and
Zinovieva, E.},
TITLE = {Symbolic Test Selection based on Approximate
Analysis},
BOOKTITLE = {11th Int. Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS'05)},
PAGES = {349-364},
YEAR = 2005,
SERIES = {LNCS},
VOLUME = 3440,
ADDRESS = {Edinburgh (Scottland)},
MONTH = avril,
ABSTRACT = {This paper addresses the problem of generating
symbolic test cases for testing the conformance of a
black-box implementation with respect to a
specification, in the context of reactive
systems. The challenge 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. Efficient
solutions to this problem have been proposed in the
context of finite-state models, based on the use of
fixpoint computations. We extend them in the
context of infinite-state symbolic models, by
showing how approximate fixpoint computations can be
used in a conservative way. The second contribution
we provide is the formalization of a quality
criterium for test cases, and a result relating the
quality of a generated test case to the
approximations used in the selection algorithm.},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/tacas05.pdf}
}
@INPROCEEDINGS{jeannet05b,
AUTHOR = {Jeannet, B. and Gopan, D. and Reps, T.},
TITLE = {A Relational Abstraction for Functions},
BOOKTITLE = {The 12th International Static Analysis Symposium,
SAS'05},
PAGES = {186--202},
SERIES = {LNCS},
VOLUME = 2672,
YEAR = 2005,
MONTH = septembre,
ABSTRACT = {This paper concerns the abstraction of sets of
functions for use in abstract interpretation. The
paper gives an overview of existing methods, which
are illustrated with applications to shape analysis,
and formalizes 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.},
DOI = {http://dx.doi.org/10.1007/11547662_14},
PDF = {http://www.irisa.fr/vertecs/Publis/Ps/2005sas.pdf}
}
@INPROCEEDINGS{komenda05a,
AUTHOR = {Komenda, J. and H.~{van Schuppen}, J. and Gaudin, B.
and Marchand, H.},
TITLE = {Modular supervisory control with general
indecomposable specification languages},
BOOKTITLE = {44nd IEEE Conference on Decision and Control
(CDC'05) and Control and European Control Conference
ECC 2005},
PAGES = {3474-3479},
YEAR = 2005,
ADDRESS = {Seville (Spain)},
MONTH = decembre,
PDF = {http://www.irisa.fr/vertecs/Publis/Ps/2005-CDC-Modular.pdf}
}
@TECHREPORT{legall05a,
AUTHOR = {{Le Gall}, T. and Jeannet, B. and Marchand, H.},
TITLE = {Contrôle de systèmes symboliques, discrets ou
hybrides},
INSTITUTION = {IRISA},
YEAR = 2005,
NUMBER = 1683,
MONTH = janvier,
ABSTRACT = {Nous abordons le problème de la synthèse de
contrôleurs à travers différents modèles allant des
systèmes de transitions finis aux systèmes hybrides
en nous intéressant à des propriétés de sûreté. Dans
ce cadre, nous nous intéressons principalement au
problème de synthèse pour un modèle intermédiaire :
les systèmes de transitions symboliques. L'analyse
des besoins de modélisation nous amène à redéfinir
la notion de contrôlabilité en faisant porter le
caractère de contrôlabilité non plus sur les
événements mais sur les gardes des transitions, puis
à définir des algorithmes de synthèse permettant
l'usage d'approximations afin d'assurer la finitude
des calculs. Nous généralisons par la suite notre
méthodologie au contrôle de systèmes hybrides, ce
qui donne un cadre unifié du problème de la synthèse
pour un ensemble consistant de modèles. },
PDF = {http://www.irisa.fr/vertecs/Publis/Ps/PI-1683.pdf}
}
@INPROCEEDINGS{legall05b,
AUTHOR = {{Le Gall}, T. and Jeannet, B. and Marchand, H.},
TITLE = {Supervisory Control of Infinite Symbolic Systems
using Abstract Interpretation},
BOOKTITLE = {44nd IEEE Conference on Decision and Control
(CDC'05) and Control and European Control Conference
ECC 2005},
YEAR = 2005,
PAGES = {31-35},
ADDRESS = {Seville (Spain)},
MONTH = decembre,
ABSTRACT = {In this paper, we investigate the control of
infinite systems, modeled by symbolic transition
system for safety properties. We first redefine the
concept of controllability by applying it to the
guards of symbolic transitions, instead of to the
events. We then define synthesis algorithms based
on symbolic transformations and abstract
interpretation techniques so that we can ensure
finiteness of the computations.},
PDF = {http://www.irisa.fr/vertecs/Publis/Ps/2005-CDC-STS.pdf}
}
@TECHREPORT{leroux05a,
AUTHOR = {Leroux, J.},
TITLE = {Structural Presburger-definable Digit Vector
Automata},
INSTITUTION = {IRISA},
YEAR = 2005,
NUMBER = 1718,
MONTH = mai,
ABSTRACT = { Digit Vector Automata (DVA) provide a natural
symbolic representation for regular sets of integer
vectors encoded as strings of digit vectors (least
significant digit first). We prove that the minimal
DVA that represents a Presburger-definable set is
structurally Presburger-definable: that means, the
DVA obtained by modifying the initial state and the
set of final states represents a
Presburger-definable set. },
PDF = {http://www.irisa.fr/vertecs/Publis/Ps/PI-1718.pdf}
}
@INPROCEEDINGS{leroux05b,
AUTHOR = {Bardin, S. and Finkel, A. and Leroux, J. and
Schnoebelen, P.},
TITLE = {Flat acceleration in symbolic model checking},
booktitle = {3rd Int. Symp. on Automated Technology for
Verification and Analysis (ATVA'05)},
pages = {474--488},
series = {LNCS},
VOLUME = 3707,
YEAR = 2005,
EDITOR = {Springer},
ADDRESS = {Taipei, Taiwan},
MONTH = octobre,
ABSTRACT = {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. In this paper we develop a new
framework for symbolic model checking with
accelerations. We also propose and analyze new
symbolic algorithms using accelerations to compute
reachability sets. Keywords: verification of
infinite-state systems, symbolic model checking,
acceleration.},
DOI = {http://dx.doi.org/10.1007/11562948_35},
PDF = {http://www.irisa.fr/vertecs/Publis/Ps/2005-ATVAa.pdf}
}
@INPROCEEDINGS{leroux05c,
AUTHOR = {Leroux, J. and Sutre, G.},
TITLE = {Flat counter automata almost everywhere!},
booktitle = {3rd Int. Symp. on Automated Technology for
Verification and Analysis (ATVA'05)},
pages = {489--503},
YEAR = 2005,
series = {LNCS},
VOLUME = 3707,
EDITOR = {Springer},
ADDRESS = {Taipei, Taiwan},
MONTH = octobre,
ABSTRACT = {This paper argues 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 show 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 prove 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).},
DOI = {http://dx.doi.org/10.1007/11562948_36},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/2005-ATVAb.pdf}
}
@INPROCEEDINGS{leroux05d,
AUTHOR = {Leroux, J. },
TITLE = {A Polynomial Time Presburger Criterion and Synthesis
for Number Decision Diagrams},
booktitle = {Proc. 20th IEEE Symp. Logic in Computer Science
(LICS'2005)},
pages = {147-156},
YEAR = 2005,
ADDRESS = {Chicago, USA},
MONTH = juin,
ABSTRACT = {Number Decision Diagrams (NDD) are the automatabased
symbolic representation for manipulating sets of
integer vectors encoded as strings of digit vectors
(least or most significant digit first). Since 1969
[8, 29], we know that any Presburger-definable set
[26] (a set of integer vectors satisfying a formula
in the first-order additive theory of the integers)
can be represented by a NDD, and efficient algorithm
for manipulating these sets have been recently
developed [31, 4]. However, the problem of deciding
if a NDD represents such a set, is a well-known hard
problem first solved by Muchnik in 1991 [23, 24, 5]
with a quadruplyexponential time algorithm. In this
paper, we show how to determine in polynomial time
whether a NDD represents a Presburger-definable set,
and we provide in this positive case a polynomial
time algorithm that constructs from the NDD a
Presburger-formula that defines the same set.},
doi = {http://dx.doi.org/10.1109/LICS.2005.2},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2005-LICS.pdf}
}
@TECHREPORT{pichardie05a,
AUTHOR = {Pichardie, D. and Rusu, V.},
TITLE = {Defining and Reasoning About General Recursive
Functions in Type Theory: a Practical Method},
INSTITUTION = {Irisa},
YEAR = 2005,
NUMBER = 1766,
MONTH = novembre,
ABSTRACT = {We propose a 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
arbitrary properties of the function. The approach
has been experimented in the Coq proof assistant,
but should work in like-minded proof asistants 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.},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/PI-1766-2.pdf}
}
@INPROCEEDINGS{rusu05a,
AUTHOR = {Rusu, Vlad and Marchand, Hervé and Jéron, Thierry},
TITLE = {Automatic Verification and Conformance Testing for
Validating Safety Properties of Reactive Systems},
BOOKTITLE = {Formal Methods 2005 (FM05)},
YEAR = 2005,
EDITOR = {Fitzgerald, John and Tarlecki, Andrzej and Hayes,
Ian},
SERIES = {LNCS},
VOLUME = 3582,
MONTH = juillet,
PUBLISHER = {Springer},
PAGES = {189-204},
DOI = {http://dx.doi.org/10.1007/11526841_14},
PDF = {http://www.irisa.fr/vertecs/Publis/Ps/final.pdf},
ABSTRACT = {This paper presents 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.}
}
@INBOOK{tschaen05a,
AUTHOR = {Tschaen, V.},
EDITOR = { Broy, M. and Jonsson, B. and Katoen, J.-P. and
Leucker, M. and Pretschner, A.},
TITLE = {Test generation algorithms based on preorder
relations},
BOOKTITLE = {Model-Based Testing of Reactive Systems},
CHAPTER = 8,
PUBLISHER = {Springer Verlag},
SERIES = {LNCS},
NUMBER = 3472,
YEAR = 2005,
ABSTRACT = {Testing theory has been studied for a long
time. Based on finite state machines at the
beginning, it has been extended to conformance
testing of transition systems. Test generation
methods have been developed for both of these
models.},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2005-Test-Chap-Book.pdf}
}