@TechReport{uppsala-report,
title = {Non-Interference on Symbolic Transition System},
author = {Dubreil, J.},
institution = {Uppsala University},
type= {Master Thesis},
month = {February},
year = {2006},
url = {http://www.irisa.fr/vertecs/Publis/Ps/report_dubreil.pdf}
}
@PhdThesis{Rusu06-hdr,
author = {Rusu, V.},
title = {Formal verification and conformance testing for reactive systems},
school = {Universit\'e de Rennes 1},
year = {2006},
month = decembre,
type = hdr,
OPTnote = {},
OPTannote = {}
}
@phdthesis{THESE-bertrand06,
author = {Bertrand, N.},
month = sep,
school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France},
type = {Th{\`e}se de doctorat},
ra = false,
title = {Mod{\`e}les stochastiques pour les pertes de messages dans les protocoles asynchrones et techniques de v{\'e}rification automatique},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-bertrand.pdf},
year = {2006},
abstract = {Asynchronous communication protocols are naturally
seen as communicating finite automata over unbounded
FIFO channels. In this thesis, we consider variants
of LCS (Lossy Channel Systems) for which message
losses are probabilistic. More precisely, we
introduce the models of Probabilistic LCS (PLCS),
and Nondeterministic and Probabilistic LCS (NPLCS)
whose semantics are respectively Markov chains and
Markov decision processes. A general criterion on
convergence of fixed points expressions in Well
Structured Transition Systems allows to prove a
number a decidability results with respect to
verification of linear-time properties for both
models. We also prove undecidability results to show
the limits of these models. A prototype tool in
OCaml implements the algorithms of this
thesis. Despite the high complexity of the problems,
this tool allows to prove liveness properties of
commmunication protocols such as the Alternating Bit
Protocol and Pachl's protocol.}
}
@inproceedings{BS05-express,
address = {San Francisco, CA, USA},
author = {Bertrand, N. and Schnoebelen, Ph.},
ra = false,
booktitle = {{P}roceedings of the 12th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'05)},
DOI = {http://dx.doi.org/10.1016/j.entcs.2006.05.007},
editor = {Baeten, Jos and Phillips, Iain},
month = jul,
number = {3},
pages = {59-69},
publisher = {Elsevier Science Publishers},
series = {Electronic Notes in Theoretical Computer Science},
title = {A short visit to the {STS} hierarchy},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BS05-express.pdf},
volume = {154},
year = {2006},
abstract = {The hierarchy of Symbolic Transition Systems,
introduced by Henzinger, Majumdar and Raskin, is an
elegant classification tool for some families of
infinite-state operational models that support some
variants of a symbolic "backward closure"
verification algorithm. It was first used and
illustrated with families of hybrid systems. In this
paper we investigate whether the STS hierarchy can
account for classical families of infinite-state
systems outside of timed or hybrid systems.}
}
@inproceedings{BBS-forte06,
address = {Paris, France},
author = {Baier, C. and Bertrand, N. and Schnoebelen, Ph.},
ra = false,
booktitle = {{P}roceedings of 26th {IFIP} {WG6.1} {I}nternational {C}onference on {F}ormal {T}echniques for {N}etworked and {D}istributed {S}ystems ({FORTE}'06)},
DOI = {http://dx.doi.org/10.1007/11888116_17},
editor = {Najm, Elie and Pradat-Peyre, Jean-Francois and Vigui{\'} Donzeau-Gouge, V{\'e}ronique},
month = sep,
pages = {212-227},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Symbolic verification of communicating systems with probabilistic message losses: liveness and fairness},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-forte06.pdf},
volume = {4229},
year = {2006},
abstract = {NPLCS’s are a new model for nondeterministic channel
systems where unreliable communication is modeled by
probabilistic message losses. We show that, for
omega-regular linear-time properties and
finite-memory schedulers, qualitative model-checking
is decidable. The techniques extend smoothly to
questions where fairness restrictions are imposed on
the schedulers. The symbolic procedure underlying
our decidability proofs has been implemented and
used to study a simple protocol handling two-way
transfers in an unreliable setting. }
}
@article{BBS-ipl06,
author = {Baier, C. and Bertrand, N. and Schnoebelen, Ph.},
DOI = {http://dx.doi.org/10.1016/j.ipl.2005.09.011},
journal = {Information Processing Letters},
ra = false,
month = jan,
number = {2},
pages = {58-63},
publisher = {Elsevier Science Publishers},
title = {A note on the attractor-property of infinite-state {M}arkov chains},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBS.pdf},
volume = {97},
year = {2006},
abstract = {In the past 5 years, a series of verification
algorithms has been proposed for infinite Markov
chains that have a finite attractor, i.e., a set
that will be visited infinitely often almost surely
starting from any state. In this paper, we establish
a sufficient criterion for the existence of an
attractor. We show that if the states of a Markov
chain can be given levels (positive integers) such
that the expected next level for states at some
level n>0 is less than n-Δ for some positive Δ, then
the states at level 0 constitute an attractor for
the chain. As an application, we obtain a direct
proof that some probabilistic channel systems
combining message losses with duplication and
insertion errors have a finite attractor.}
}
@TechReport{pass,
author = {Breunesse, C. and Hubbers, E. and Koopman, P. and Mostowski, W. and Oostdijk, M. and Rusu, V. and de~Vries, R. and van~Weelden, A. and Wichers~Schreur, R. and Willemse, T.},
title = {Testing the Dutch e-passport},
institution = {Radboud University, Nijmegen, The Netherlands},
year = {2006}
}
@ARTICLE{rusu-computer-journal,
AUTHOR = {Rusu, v.},
TITLE = {Verifying an ATM Protocol Using a Combination of Formal Techniques},
JOURNAL = {Computer Journal},
YEAR = {2006},
VOLUME = {49},
NUMBER = {6},
PAGES = {710-730},
MONTH = novembre,
ABSTRACT = { This paper describes 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.},
doi={http://dx.doi.org/10.1093/comjnl/bxl039}
}
@InBook{I2C-constant-jeron-marchand-rusu-06,
author = {Constant, C. and J\'eron, T. and Marchand, H. and Rusu, V.},
title = {Combinaison entre v\'erification et test pour la validation de syst\`emes r\'eactifs},
booktitle = {Trait\'e I2C. Syst\`emes Temps R\'eel: Techniques de Description et
de V\'erification - Th\'eorie et Outils},
chapter = {2},
publisher = {Herm\`es Science},
year = {2006},
volume = {1}
pages = {59-88}
}
@InProceedings{komenda06a,
author = {Komenda, J. and Marchand, H. and Pinchinat, S.},
title = {A constructive and modular approach to decentralized supervisory Control problems},
booktitle = {3rd IFAC Workshop on Discrete-Event System Design},
year = {2006},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2006-C-DESDes.pdf},
Abstract ={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.}
}
@INPROCEEDINGS{Jeron-DIPES06,
AUTHOR = {J\'eron, Thierry},
TITLE = {Model-based test selection for infinite state reactive systems},
BOOKTITLE = {5th IFIP Working Conference on Distributed and Parallel Embedded Systems, DIPES'06, Braga, Portugal},
YEAR = {2006},
MONTH = octobre,
PUBLISHER = {Springer SBM},
NOTE = {Invited paper},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/dipes06.pdf}
}
@INPROCEEDINGS{LeGall-Jeannet-Jeron-AMAST06,
AUTHOR ={Le Gall, T. and Jeannet, B. and J\'eron, T.},
TITLE = {Verification of Communication Protocols using Abstract Interpretation of FIFO queues},
BOOKTITLE = {11th International Conference on Algebraic Methodology and Software Technology, AMAST '06, Kuressaare, Estonia},
EDITOR ={Michael Johnson and Varmo Vene},
YEAR = {2006},
MONTH = juillet,
SERIES = {LNCS},
VOLUME = {4019},
PAGES = {204-219},
PUBLISHER = {Springer-Verlag},
asbtract = {We address 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.},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/amast06.pdf},
doi= {http://dx.doi.org/10.1007/11784180_17},
}
@INPROCEEDINGS{flop-barthe-forest-pichardie-rusu-06,
AUTHOR = {Barthe, G. and Forest, J. and Pichardie, D. and Rusu, V.},
BOOKTITLE = {Functional and LOgic Programming Systems (FLOPS'06)},
TITLE = {Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant},
YEAR = {2006},
ADDRESS = {Fuji Susono, Japan},
MONTH = avril,
PAGES = {114-129},
SERIES = {LNCS},
VOLUME = {3945},
ABSTRACT= {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.},
doi= {http://dx.doi.org/10.1016/10.1007/11737414_9},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2006-FLOPS.pdf}
}
@TECHREPORT{jeron-marchand-rusu-pi-deter-06,
AUTHOR = {J\'eron, T. and Marchand, H. and Rusu, V. },
TITLE = {Symbolic Determinisation of Extended Automata },
INSTITUTION = {IRISA},
YEAR = {2006},
NUMBER = {1176},
MONTH = fevrier,
ABSTRACT = {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.},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/PI-1776.pdf}
}
@INPROCEEDINGS{jeron-marchand-rusu-tcs-deter-06,
AUTHOR = {J\'eron, T. and Marchand, H. and Rusu, V.},
TITLE = {Symbolic Determinisation of Extended Automata},
BOOKTITLE = {4th IFIP International Conference on Theoretical Computer Science},
PUBLISHER = {Springer Science and Business Media},
SERIES = {IFIP book series},
YEAR = {2006},
DOI = {http://dx.doi.org/10.1007/978-0-387-34735-6_18},
PAGES = {197-212},
ADDRESS = {Stantiago, Chile},
MONTH = aout,
ABSTRACT = {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.},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/TCS-2006-deter.pdf}
}
@TECHREPORT{pi-jeron-marchand-pinchinat-cordier-06,
AUTHOR = {J\'eron, T. and Marchand, H. and Pinchinat, S. and Cordier, M-O.},
TITLE = {Supervision Patterns in Discrete Event Systems Diagnosis},
INSTITUTION = {IRISA},
YEAR = {2006},
NUMBER = {1784},
MONTH = fevrier,
ABSTACT ={In this paper, 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 diagnosticability
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.},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/PI-1784.pdf}
}
@INPROCEEDINGS{wodes-jeron-marchand-pinchinat-cordier-06,
AUTHOR = {J\'eron, T. and Marchand, H. and Pinchinat, S. and Cordier, M-O.},
TITLE = {Supervision Patterns in Discrete Event Systems Diagnosis},
BOOKTITLE = {Workshop on Discrete Event Systems, WODES'06},
YEAR = {2006},
ADDRESS = {Ann-Arbor (MI, USA)},
MONTH = juillet,
pages = {262-268},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2006-Wodes-Diag.pdf},
doi = {http://dx.doi.org/10.1016/10.1109/WODES.2006.1678440},
NOTE = {Also published in DX'06,
Penaranda de Duero (Burgos, Spain)},
ABSTRACT = {In this paper, 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 a supervision pattern 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 diagnosticability
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.}
}
@INPROCEEDINGS{rfia-jeron-marchand-cordier-06,
AUTHOR = {J\'eron, T. and Marchand, H. and Cordier, M-O.},
TITLE = {Motifs de surveillance pour le diagnostics de syst\`emes à \'ev\'enements discrets finis},
BOOKTITLE = {15e congr\`es francophone AFRIF-AFIA Reconnaissance des Formes et Intelligence Artificielle},
YEAR = {2006},
CONFNAT = true,
ADDRESS = {Tours, France},
MONTH = janvier,
ABSTRACT = {Dans cet article, nous nous int\'eressons au diagnostic dans les
syst\`emes de transition finis. Nous proposons un mod\`ele de motifs de
surveillance correspondant à des propri\'et\'es d'atteignabilit\'e. Ceci permet de
g\'en\'eraliser les propri\'et\'es à diagnostiquer tout en les d\'ecouplant de la
description du syst\`eme. Nous en d\'eduisons des techniques de v\'erification de
diagnosticabilit\'e et de construction de diagnostiqueur fond\'ees sur des
op\'erations standards sur les syst\`emes de transitions. Nous montrons que ces
techniques sont suffisamment g\'en\'erales pour exprimer et r\'esoudre de mani\`ere
unifi\'ee une classe importante de probl\`emes de diagnostic consid\'er\'es dans la
litt\'erature comme le diagnostic de pannes permanentes, de pannes multiples,
de s\'equences de pannes, et certains probl\`emes de diagnostic de pannes
intermittentes.},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/2006-RFIA-Diag.pdf}
}
@ARTICLE{tsi-legall-jeannet-marchand-06,
AUTHOR = {Le Gall, T. and Jeannet, B. and Marchand, H.},
TITLE = {Contr\^ole de syst\`emes symboliques, discrets ou hybrides},
JOURNAL = {Technique et Science Informatiques (TSI)},
YEAR = {2006},
VOLUME = {25},
NUMBER = {3},
PAGES = {293-319},
ABSTRACT = {Nous abordons le probl\`eme de la synth\`ese de contr\^oleurs \`a
travers diff\'erents mod\`eles allant des syst\`emes de transitions finis
aux syst\`emes hybrides en nous int\'eressant à des propri\'et\'es de
sûret\'e. Dans ce cadre, nous nous int\'eressons principalement au
probl\`eme de synth\`ese pour un mod\`ele interm\'ediaire~: les syst\`emes de
transitions symboliques. L'analyse des besoins de mod\'elisation nous
am\`ene à red\'efinir la notion de contr\^olabilit\'e en faisant porter le
caract\`ere de contr\^olabilit\'e non plus sur les \'ev\'enements mais sur les
gardes des transitions, puis \`a d\'efinir des algorithmes de synth\`ese
permettant l'usage d'approximations et d'assurer la terminaison des
calculs. Nous g\'en\'eralisons par la suite notre m\'ethodologie au
contr\^ole de syst\`emes hybrides, ce qui donne un cadre unifi\'e du
probl\`eme de la synth\`ese pour un ensemble consistant de mod\`eles.},
OPTmonth = {},
doi = {http://dx.doi.org/10.3166/tsi.25.289-315},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/2006-TSI-STS.pdf}
}
@INPROCEEDINGS{wodes-schmidt-marchand-gaudin-06,
AUTHOR = {Schmidt, K. and Marchand, H. and Gaudin., B.},
TITLE = {Modular and Decentralized Supervisory Control of Concurrent Discrete Event Systems Using Reduced System
Models},
BOOKTITLE = {Workshop on Discrete Event Systems, WODES'06},
YEAR = {2006},
PAGES = {149-154},
ADDRESS = {Ann-Arbor (MI, USA)},
MONTH = juillet,
ABSTRACT = {This work investigates 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.
},
DOI = {http://dx.doi.org/10.1109/WODES.2006.1678423},
pdf = {http://www.irisa.fr/vertecs/Publis/Ps/2006-Wodes_modular.pdf}
}
@Misc{besnard06a,
author = {Besnard, L. and Marchand, H. and Rutten, E.},
title = {The Sigali Tool Box Environment},
howpublished = {Workshop on Discrete Event Systems, WODES'06 (Tool Paper)},
YEAR = {2006},
ADDRESS = {Ann-Arbor (MI, USA)},
MONTH = juillet,
PAGES = {465-466},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/2006-Tool-Wodes-Sigali.pdf}
}
@Misc{V3F-rapport-final-2006,
author = {Legeard, Bruno and Rueher, Michel and J\'eron, Thierry and Marre, Bruno},
title = {V3F: Validation et V\'erification en pr\'esence de calculs à Virgule Flottante},
howpublished = {Rapport final de l'Action Concert\'ee Incitative, S\'ecurit\'e Informatique},
month = octobre,
year = {2006}
}
@InProceedings{V3F_CSTVA06,
author = {Blanc, B. and Bouquet, F. and Gotlieb, A. and Jeannet, B. and J\'eron, T. and Legeard, B. and Marre, B. and Michel, C. and Rueher, M.},
title = {The {V3F} Project},
booktitle = {Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA06), Nantes},
year = {2006},
editor = {Blanc, B. and Gotlieb, A. and Michel, C.},
URL = {http://www.irisa.fr/manifestations/2006/CSTVA06/images/proceedings-cstva.pdf},
Abstract = {This paper describes the main results of the V3F project
(which stands for “Validation and verification of software handling float-
ing-point numbers”). The goal of this project was to provide tools to
support the verification and validation process of programs with floating-
point numbers. We did investigate two directions: structural testing of
a program with floating-point numbers and verification of the confor-
mity of a program handling floating-point numbers, with its specification.
Practically, a constraint solver over the floats was developed for the gen-
eration of test sets in structural testing framework. Different techniques
have been developed to evaluate the distance between the semantics of a
program over the real numbers and its semantics over the floating-point
numbers.}
}