@TechReport{rc07,
author = {Rusu, V. and Clavel, M.},
title = {Theorem proving for Maude's Rewriting Logic},
institution = {Irisa},
year = 2007,
number = {1873},
abstract = {We present an approach based on inductive theorem
proving for verifying invariance properties of
systems specified in Rewriting Logic, an executable
specification language implemented (among others) in
the Maude tool. Since theorem proving is not
directly available for rewriting logic, we define an
encoding of rewriting logic into its membership
equational (sub)logic. Then, inductive theorem
provers for membership equational logic, such as the
ITP tool, can be used for verifying the resulting
membership equational logic specification, and,
implicitly, for verifying invariance properties of
the original rewriting logic specification. The
approach is illustrated first on a 2-process Bakery
algorithm and then on a parameterised, n-process
version of the algorithm.},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/PI-1873.pdf}
}
@inproceedings{BBBBG-fsttcs07,
address = {New~Delhi, India},
author = {Baier, C. and Bertrand, N. and Bouyer, P. and
Brihaye, Th. and Groesser, M.},
ra = false,
booktitle = {{P}roceedings of the 27th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'07)},
editor = {Arvind, V. and Prasad, Sanjiva},
month = decembre,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Probabilistic and Topological Semantics for Timed Automata},
doi = {http://dx.doi.org/10.1007/978-3-540-77050-3_15},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBBG-fsttcs07.pdf},
volume = 4855,
year = 2007,
pages = {1529-3785},
abstract = {Like most models used in model-checking, timed
automata are an idealized mathematical model used
for representing systems with strong timing
requirements. In such mathematical models,
properties can be violated, due to unlikely
(sequences of) events. We propose two new semantics
for the satisfaction of LTL formulas, one based on
probabilities, and the other one based on topology,
to rule out these sequences. We prove that the two
semantics are equivalent and lead to a
PSPACE-Complete model-checking problem for LTL over
finite executions.},
x-international-audience ={yes},
x-proceedings ={yes}
}
@article{BBS-arxiv07,
author = {Baier, C. and Bertrand, N. and Schnoebelen, Ph.},
journal = {ACM Transactions on Computational Logic},
number = 1,
publisher = {ACM Press},
ra = false,
title = {Verifying nondeterministic probabilistic channel
systems against omega-regular linear-time
properties},
doi = {http://dx.doi.org/10.1145/1297658.1297663},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/acm07.pdf},
volume = 9,
year = 2007,
abstract = {Lossy channel systems (LCS’s) are systems of finite
state processes that communicate via unreliable
unbounded fifo channels. We introduce NPLCS’s, a
variant of LCS’s where message losses have a
probabilistic behavior while the component processes
behave nondeterministically, and study the
decidability of qualitative verification problems
for omega-regular linear-time properties. We show
that – in contrast to finite-state Markov decision
processes – the satisfaction relation for lineartime
formulas depends on the type of schedulers that
resolve the nondeterminism. While the qualitative
model checking problems for the full class of
history-dependent schedulers is undecidable, the
same questions for finitememory schedulers can be
solved algorithmically. Additionally, some special
kinds of reachability, or recurrent reachability,
qualitative properties yield decidable verification
problems for the full class of schedulers, which –
for this restricted class of problems – are as
powerful as finite-memory schedulers, or even a
subclass of them.},
x-international-audience ={yes},
x-proceedings ={yes},
x-editorial-board ={yes}
}
@Article{ieee-tse,
author = {Constant, C. and J\'eron, T. and Marchand, H. and
Rusu, V.},
title = {Integrating formal verification and conformance
testing for reactive systems},
journal = {IEEE Transactions on Software Engineering},
year = 2007,
volume = 33,
number = 8,
pages = {558-574},
month = aout,
absrtact = {In this paper, we describe a methodology integrating
verification and conformance testing. 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.},
doi = {http://dx.doi.org/10.1109/TSE.2007.70707},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2007-IEEE-TSE.pdf},
x-international-audience ={yes},
x-proceedings ={yes},
x-editorial-board ={yes}
}
@InProceedings{legall-jeannet-sas,
author = {Le Gall, T. and Jeannet, B.},
title = {Lattice automata: a representation of languages over
an infinite alphabet, and some applications to
verification},
booktitle = {The 14th International Static Analysis Symposium,
SAS 2007},
pages = {52-68},
year = 2007,
volume = 4634,
series = {LNCS},
address = {Kongens Lyngby, Denmark},
month = aout,
abstract = {This paper proposes a new abstract domain for
languages on infinite alphabets, which acts as a
functor taking an abstract domain for a concrete
alphabet and lift it to an abstract domain for words
on this alphabet. The abstract representation is
based on lattice automata, which are finite automata
labeled by elements of an atomic lattice. We define
a normal form, standard language operations and a
widening operator for these automata. We apply this
abstract lattice for the verification of symbolic
communicating machines, and we discuss its
usefulness for interprocedural analysis.},
doi = {http://dx.doi.org/10.1007/978-3-540-74061-2_4},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2007-SAS.pdf},
x-international-audience ={yes},
x-proceedings ={yes}
}
@InProceedings{dubreil-msr,
author = {Dubreil, J. and J\'eron, T. and Marchand, H.},
title = {Construction de moniteurs pour la surveillance de
propri\'et\'es de s\'ecurit\'e},
booktitle = {6\`eme Colloque Francophone sur la Mod\'elisation
des Syst\`emes R\'eactifs},
confnat = true,
year = 2007,
pages = {105-120},
address = {Lyon, France},
month = octobre,
abstract = {Nous nous intéressons à la construction de moniteurs
permettant de détecter la fuite d'information
confidentielle pour des systèmes partiellement
observables, modélisés par des systèmes de
transition finis. Nous considérons le cas où le
secret peut se modéliser par des langages réguliers.
Nous commençons par définir la notion d'opacité pour
formaliser la fuite d'information. Nous
caractérisons l'ensemble des observations pour
lesquelles un attaquant infère de l'information
confidentielle. En adaptant les techniques de
diagnostic sur des systèmes à événement discrets,
nous explicitons des conditions nécessaires et
suffisantes sur le système pour permettre la
détection et/ou la prédiction de cette fuite
d'information et construisons un moniteur permettant
un administrateur d'assurer cette détection. Nous
considérons le cas général où l'attaquant et
l'administrateur ont des vues partielles différentes
du système.},
URL =
{http://www.irisa.fr/vertecs/Publis/Ps/2007-MSR-Opacity.pdf},
x-international-audience ={yes},
x-proceedings ={yes}
}
@InProceedings{dumitrescu-msr,
author = {Dumitrescu, E. and Girault, A. and Marchand, H. and
Rutten, E.},
title = {Synth\`ese optimale de contr\^oleurs discrets et
syst\`emes r\'epartis tol\'erants aux fautes},
booktitle = {6\`eme Colloque Francophone sur la Mod\'elisation
des Syst\`emes R\'eactifs},
year = 2007,
pages = {71-86},
confnat = true,
address = {Lyon, France},
month = octobre,
abstract = {Les systèmes embarqués requièrent des méthodes de
conception sûres fondées sur des méthodes formelles,
ainsi qu'une exécution sûre fondée sur des
techniques de tolérance aux fautes. Nous proposons
une méthode de conception sûre pour des systèmes à
l'exécution sûre: elle utilise la synthèse de
contrôleurs discrets (SCD) pour générer un système
tolérant aux fautes, reconfigurable et correct. Les
propriétés assurées concernent l'exécution
consistante, l'assurance de la fonctionnalité
(quelles que soient les fautes, sous une certaine
hypothèse), et plusieurs optimisations, notamment
sur le temps des exécutions passant par des points
de reprise. Nous proposons un algorithme de SCD
optimale sur des chemins bornés. Nous proposons des
motifs de modèles pour des tâches, des processeurs à
mémoire répartie et des motifs de fautes
potentiels. Nous utilisons des modèles synchrones,
l'outil de SCD symbolique Sigali et les Automates de
Modes.},
URL =
{http://www.irisa.fr/vertecs/Publis/Ps/2007-MSR-TAF.pdf},
x-international-audience ={yes},
x-proceedings ={yes}
}
@TechReport{legall07,
author = {Le Gall, T. and Jeannet, B.},
title = {Analysis of Communicating Infinite State Machines
using Lattice Automata},
institution = {IRISA},
year = 2007,
number = 1839,
month = mars,
abstract = {Communication protocols can be formally described by
the Communicating Finite-State Machines~(CFSM)
model. This model is expressive, but not expressive
enough to deal with complex protocols that involve
structured messages encapsulating integers or lists
of integers. This is the reason why we propose an
extension of this model : the Symbolic Communicating
Machines (SCM). We also propose an approximate
reachability analysis method, based on lattice
automata. Lattice automata are finite automata, the
transitions of which are labeled with elements of an
atomic lattice. We tackle the problem of the
determinization as well as the definition of a
widening operator for these automata. We also show
that lattice automata are useful for the
interprocedural analysis.},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/PI-1839.pdf}
}
@Article{deds-gaudin-marchand-07,
author = {Gaudin, B. and Marchand, H.},
title = {An Efficient Modular Method for the Control of
Concurrent Discrete Event Systems: A Language-Based
Approach},
journal = {Discrete Event Dynamic System},
year = 2007,
volume = 17,
number = 2,
pages = {179-209},
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 investigate the
computation of the supremal controllable language
contained in the language of the specification. 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
specification. It is shown that, under some
assumptions, 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 having to build 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 the class of
separable specifications.},
doi = {http://dx.doi.org/10.1007/s10626-006-0007-7},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2007-JDEDS.pdf},
x-international-audience ={yes},
x-proceedings ={yes},
x-editorial-board ={yes}
}
@INPROCEEDINGS{JJR-FMCO-06,
author = {Jeannet, B. and J\'{e}ron, T. and Rusu, V.},
title = {Model-based test selection for infinite state
reactive systems},
booktitle = {{Formal Methods of Components and Objects -- FMCO
2006, Amsterdam, Netherlands, Revised Lectures}},
OPTeditor = {de~Boer, F.S and Bonsangue, M. M. and Graf, S. and
de~Roever, W.-P.},
year = 2007,
pages = {47--69},
series = {LNCS},
volume = 4709,
publisher = {Springer},
x-international-audience ={yes},
x-proceedings ={yes},
abstract= {This paper addresses the problem of off-line selection of
test cases for testing the conformance of a
black-box implementation with respect to a
specification, in the context of reactive
systems. Efficient solutions to this problem have
been proposed in the context of finite-state models,
based on the ioco conformance testing theory. An
extension of these is proposed in the context of
infinite-state specifications, modelled as automata
extended with variables. One considers the selection
of test cases according to test purposes describing
abstract scenarios that one wants to test. The
selection of program test cases then consists in
syntactical transformations of the specification
model, using approximate analyses.},
doi = {http://dx.doi.org/10.1007/978-3-540-74792-5_3},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/fmco06.pdf}
}
@Misc{ployette07,
Author = {Ployette, F. and Jeannet, B. and J\'eron, T.},
Title = {Stg: a symbolic test generation tool for reactive
systems},
Howpublished = {TESTCOM/FATES07 (Tool Paper)},
Address = {Tallinn, Estonia},
Month = {June},
Year = 2007
}
@InProceedings{TestCom07,
author = {Constant, C. and Jeannet, B. and J\'eron, T.},
title = {Automatic test generation from interprocedural
specifications},
booktitle = {TestCom/Fates07},
month = juin,
year = 2007,
series = {LNCS},
volume = 4581,
pages = {41-57},
address = {Tallinn, Estonia},
abstract = {This paper adresses the generation of test cases for
testing the conformance of a reactive black-box
implementation with respect to its specification. We
aim at extending the principles and algorithms of
model-based testing for recursive interprocedural
specifications that can be modeled by Push-Down
Systems (PDS). Such specifications may be more
compact than non-recursive ones and are more
expressive. The generated test cases are selected
according to a test purpose, a (set of) scenario of
interest that one wants to observe during test
execution. The test generation method we propose in
this paper is based on program transformations and a
coreachability analysis, which allows to decide
whether and how the test purpose can still be
satisfied. However, despite the possibility to
perform an exact analysis, the inability of test
cases to inspect their own stack prevents it from
using fully the coreachability information. We
discuss this partial observation problem, its
consequences, and how to minimize its impact.},
doi = {http://dx.doi.org/10.1007/978-3-540-73066-8_4},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2007-Testcom.pdf},
x-international-audience ={yes},
x-proceedings ={yes}
}
@TechReport{Dumitrescu07a,
author = {Dumitrescu, E. and Girault, A. and Marchand, H. and
Rutten, E.},
title = {Optimal discrete controller synthesis for the
modeling of fault-tolerant distributed systems},
institution = {INRIA},
year = 2007,
number = 6137,
month = mars,
abstract = {Embedded systems require safe design methods based
on formal methods, as well as safe execution based
on fault-tolerance techniques. We propose a safe
design method for safe execution systems: it uses
optimal discrete controller synthesis (DCS) to
generate a correct reconfiguring fault-tolerant
system. The properties enforced concern consistent
execution, functionality fulfillment (whatever the
faults, under some failure hypothesis), and several
optimizations, particularly on the execution time
when going through checkpoints. We propose an
algorithm for optimal DCS on bounded paths. We
propose model patterns for a set of periodic tasks
with checkpoints, a set of distributed,
heterogeneous and fail-silent processors, and an
environment model that expresses the potential fault
patterns. We use synchronous models, the Sigali
symbolic DCS tool and Mode Automata.},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/RR-6137.pdf}
}
@InProceedings{ifm2007,
author = {Oostdijk, M. and Rusu, V. and Tretmans, J. and
{de~Vries}, R. and Willemse, T.},
title = {Integrating verification, testing, and learning for
cryptographic protocols},
booktitle = {Integrated Formal Methods (IFM'07)},
year = 2007,
series = {Lecture Notes in Computer Science},
publisher = {Springer Verlag},
abstract = {The verification of cryptographic protocol
specifications is an active research topic and has
received much attention from the formal verification
community. By contrast, the black-box testing of
actual implementations of protocols, which is,
arguably, as important as verification for ensuring
the correct functioning of protocols in the “real”
world, is little studied. We propose an approach for
checking secrecy and authenticity properties not
only on protocol specifications, but also on
black-box implementations. The approach is
compositional and integrates ideas from
verification, testing, and learning. It is
illustrated on the Basic Access Control protocol
implemented in biometric passports.},
doi = {http://dx.doi.org/10.1007/978-3-540-73210-5_28},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2007-IFM.pdf},
x-international-audience ={yes},
x-proceedings ={yes}
}
@InProceedings{Dumitrescu07b,
author = {Dumitrescu, E. and Girault, A. and Marchand, H. and
Rutten, E.},
title = {Optimal discrete controller synthesis for the
modeling of fault-tolerant distributed systems},
booktitle = {First IFAC Workshop on Dependable Control of
Discrete Systems (DCDS'07)},
year = 2007,
address = {Paris, France},
month = juin,
URL = {http://www.irisa.fr/vertecs/Publis/Ps/RR-6137.pdf},
x-international-audience ={yes},
x-proceedings ={yes}
}
@TechReport{PI-jeron07a,
author = {J\'eron, T. and Marchand, H. and Genc, S. and
Lafortune, S.},
title = {Predictability of Sequence Patterns in Discrete
Event Systems},
institution = {IRISA},
year = 2007,
number = 1834,
month = mars,
abstract = {The problem of predicting the occurrences of a
pattern in a partially-observed discrete-event
system is studied. The system is modeled by a
labeled transition system. The pattern is a set of
event sequences modeled by a finite-state
automaton. The occurrences of the pattern are
predictable if it is possible to infer about any
occurrence of the pattern before the pattern is
completely executed by the system. An off-line
algorithm to verify the property of predictability
is presented. The verification is polynomial in the
number of states of the system. An on-line
algorithm to track the execution of the pattern
during the operation of the system is also
presented. This algorithm is based on the use of a
diagnoser automaton. The results are illustrated
using an example from computer systems.},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/PI-1834.pdf}
}
@TechReport{PI-Constant07a,
author = {Constant, C. and Jeannet, B. and J\'eron, T.},
title = {Automatic Test Generation from Interprocedural
Specifications},
institution = {IRISA},
year = 2007,
number = 1835,
month = mars,
abstract = {This paper adresses the generation of test cases for
testing the conformance of a black-box
implementation with respect to its speci cation, in
the context of reactive systems. We aim at extending
the principles and algorithms of model-based testing
a la ioco for recursive speci cations that can be
modeled by Push-Down Systems (PDS). Such speci
cations may be more compact than non-recursive ones
and are more expressive. The generated test cases
are selected according to a test purpose, a (set of)
scenario of interest that one wants to observe
during test execution. The test generation method we
propose in this paper is based on program
transformations and a coreachability analysis, which
allows to decide whether and how the test purpose
can still be satis ed. However, despite the
possibility to perform an exact analysis, the
inability of test cases to inspect their own stack
prevents it from using fully the coreachability
information. We discuss this partial observation
problem, its consequences, and how to minimize its
impact.},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/PI-1835.pdf}
}
@Article{PJJJLT-TSE07,
author = {Pickin, S. and Jard, C. and J\'eron, T. and
J\'ez\'equel, J-M and Le~Traon, Y.},
title = {Test Synthesis from UML Models of Distributed
Software},
journal = {IEEE Transactions on Software Engineering},
year = 2007,
volume = 33,
number = 4,
month = avril,
pages = {252-269},
abstract = {The object-oriented software development process is
increasingly used for the construction of complex
distributed systems. In this context, behavior
models have long been recognized as the basis for
systematic approaches to requirements capture,
specification, design, simulation, code generation,
testing, and verification. Two complementary
approaches for modeling behavior have proven useful
in practice: interaction-based modeling (e.g. UML
sequence diagrams) and state-based modeling
(e.g. UML statecharts). Building on formal V&V
techniques, in this article we present a method and
a tool for automated synthesis of test cases from
scenarios and a state-based design model of the
application, remaining entirely within the UML
framework. The underlying ?on the fly? test
synthesis algorithms are based on the input/output
labeled transition system formalism, which is
particularly appropriate for modeling applications
involving asynchronous communication. The method is
eminently compatible with classical OO development
processes since it can be used to synthesize test
cases from the scenarios used in early development
stages to model global interactions between actors
and components, instead of these test cases being
derived manually. We illustrate the system test
synthesis process using an Air Traffic Control
software example.},
doi = {http://dx.doi.org/10.1109/TSE.2007.39},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2007-IEEE-TSE-UML.pdf},
x-international-audience ={yes},
x-proceedings ={yes},
x-editorial-board ={yes}
}
@Misc{xgsfgs
}