@InProceedings{cjrz01a,
author = {Clarke, D. and Jéron, T. and Rusu, V. and Zinovieva, E. },
title = {Automated Test and Oracle Generation for Smart-Card Applications},
booktitle = {International Conference on Research in Smart Cards (e-Smart'01), Volume 2140 of LNCS},
year = {2001},
pages ={58-70},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/2001-ESMART.ps.gz},
THEMES = {symb-testing,STG,case-study}
}
@inproceedings{cjrz01b,
author = {Clarke, D. and Jéron, T. and Rusu, V. and Zinovieva, E. },
title = {STG : A Tool for Generating Symbolic Test Programs and Oracles
from Operational Specifications},
booktitle = {Joint 8th European Software Engineering Conference (ESEC) and
9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-9)},
year = {2001},
page = {301-302},
THEMES = {STG,symb-testing}
}
@INPROCEEDINGS{jeannet01a,
AUTHOR = {{D'Argenio}, {P.R.} and Jeannet, B. and Jensen, {H.E.} and Larsen, {K.J.}},
TITLE={Reachability Analysis of Probabilistic Systems by Successive Refinements},
BOOKTITLE={Process Algebra and Probabilistic Methods - Performance Modelling and Verification, PAPM-PROBM 2001},
address={Aachen, Germany},
series = {LNCS},
volume = {2165},
month = septembre,
year=2001,
ABSTRACT ={We report on a novel development to model check quantitative
reachability properties on Markov decision processes together with its
prototype implementation. The innovation of the technique is that the
analysis is performed on an abstraction of the model under
analysis. Such an abstraction is significantly smaller than the original
model and may safely refute or accept the required property. Otherwise,
the abstraction is refined and the process repeated. As the numerical
analysis necessary to determine the validity of the property is more
costly than the refinement process, the technique profits from applying
such numerical analysis on smaller state spaces. },
URL={http://www.irisa.fr/prive/bjeannet/djjl01.ps.gz}
}
@Article{marchand01a,
author = {Marchand, H. and Rutten, E. and {Le Borgne}, M. and Samaan, M.},
title = {Formal Verification of programs specified with SIGNAL : Application to a Power Transformer Station Controller},
journal = {Science of Computer Programming},
year = {2001},
VOLUME = {41},
NUMBER = {1},
MONTH = aout,
PAGES = {85--104},
DOI = {http://dx.doi.org/10.1016/S0167-6423(00)00020-4},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/2001-JSCP.pdf},
ABSTRACT = {We present a formal specification and verification of the
automatic circuit-breaking behavior of an electric power transformer station,
using the synchronous approach to reactive real-time systems implemented by the
data-flow language Signal. Synchronous languages have a mathematical model
that supports the various phases of the development of a control system:
specification, verification, simulation, code generation, and implementation.
The complex hierarchical, state-based and preemptive behavior of the power
station controller is specified in Signalgti, an extension of Signal with
notions of time intervals and preemptive tasks. To validate the specification,
a graphical simulator is generated using Signal's execution environment, and
the required behaviour is proven to be satisfied, using its proof method.}
}
@INPROCEEDINGS{marchand01b,
AUTHOR = {Marchand, H. and Boivineau, O. and Lafortune, S.},
TITLE = {Optimal control of discrete event systems under partial observation},
BOOKTITLE = {40th IEEE Conference on Decision and Control},
YEAR = {2001},
MONTH = decembre,
PAGES = {2235--2240},
ADDRESS = {Orlando, Florida, USA},
ABSTRACT = {
We are interested in a new class of optimal control problems for Discrete Event
Systems (DES). We adopt the classical formalism of supervisory control theory
and model the system as a finite state machine (FSM). Our control problem is
characterized by the presence of uncontrollable as well as unobservable events,
the notion of occurrence and control costs for events and a worst-case
objective function. We first derive an observer for the partially unobservable
FSM, which allows us to construct an approximation of the unobservable
trajectory costs. We define the performance measure on this observer rather
than on the original FSM itself. Further, we use the algorithm of [Sengupta &
Lafortune, Siam Control and Optimisation, 36(2), 1998] to synthesize an optimal
submachine of the observer. This submachine leads to the desired supervisor
for the system.},
doi = {http://dx.doi.org/10.1109/.2001.980609},
URL = {http://www.irisa.fr/vertecs/Publis/Ps/2001-CDC-Opt.pdf}
}
@INPROCEEDINGS{benveniste01a,
AUTHOR = {Benveniste, A. and Bournai, P. and Gautier, T. and {Le Borgne}, M. and {Le Guernic}, P. and Marchand, H.},
TITLE = {The Signal declarative synchronous language : controller synthesis & systems/architecture design},
BOOKTITLE = {40th IEEE Conference on Decision and Control},
YEAR = {2001},
MONTH = {December},
ADDRESS = {Orlando, Florida, USA},
PAGES = {3284--3289},
ABSTRACT = {Harel and Pnueli showed (1985) that dynamical systems are an essential in the area of computer science. In this context they are called reactive systems. Synchronous languages have been proposed as a paradigm to deal with reactive systems and develop tools for them. In this paper we introduce synchronous programming paradigm via the notion of multiclock dynamical systems and illustrate it via the SIGNAL language. We give an outline of controller synthesis in SIGNAL, and system/architecture design},
doi = {http://dx.doi.org/10.1109/.2001.980328 },
URL = {http://www.irisa.fr/vertecs/Publis/Ps/2001-CDC-Signal.pdf}
}
@INPROCEEDINGS{r01a,
AUTHOR = {Rusu, V. },
TITLE = {Verifying that Invariants are Context-Inductive},
BOOKTITLE = {Theorem Proving in Higher-Order Logics (TPHOLs'01),, Category B paper, University of Edinburgh research Report EDI-INF-RR-0046},
YEAR = {2001},
PAGES = {337-351},
ABSTRACT = {
We study the deductive verification of infinite-state systems modeled by
extended automata. Typically, this process requires proving many invariants,
and automatically discharging these proof obligations would save the user a
significant amount of effort. To accomplish this we present techniques for
automatically verifying that invariants are inductive in a given context, and
identify a class of systems and a logic for expressing invariants and contexts
for which the problem is decidable.},
URL={http://www.irisa.fr/vertecs/Publis/Ps/2001-TPHOL.ps.gz}
}
@INPROCEEDINGS{r01b,
AUTHOR = {Rusu, V.},
TITLE = {Verifying a Sliding-Window Protocol using PVS},
BOOKTITLE = {Formal Description Techniques (FORTE'01)},
PAGES= {251-266},
YEAR = {2001},
ABSTRACT = {We present the deductive verification of safety and liveness properties
of a sliding-window protocol using the PVS theorem prover. The protocol
is modeled in an operational style which is close to an actual program.
It has parametric window sizes for both sender and receiver, and unbounded
lossy communication channels carrying unbounded data. The proofs are done
using invariant strengthening techniques encoded as PVS automated strategies
based on heuristics and decision procedures.
},
URL={http://www.irisa.fr/vertecs/Publis/Ps/Forte01.ps.gz}
}
@TechReport{rusu01,
author = {Rusu, V.},
title = {Analyzing Automata with Presburger Arithmetic and Uninterpreted
Function Symbols},
institution = {INRIA},
year = {2001},
number = {4100},
abstract = {We study a class of extended automata defined by guarded commands over Presburger arithmetic with uninterpreted functions. On the theoretical side, we show that the bounded reachability problem is decidable in this model. On the practical side, the class is useful for modeling programs with potentially infinite data structures, and the reachability procedure can be used for symbolic simulation, testing, and verification.},
url = {ftp://ftp.inria.fr/INRIA/publication/publi-ps-gz/RR/RR-4100.ps.gz}
}
@Article{rz01,
author = {Rusu, V. and Zinovieva, E. },
title = {Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols},
journal = {Electronic Notes in Theoretical Computer Science},
year = {2001},
volume = {50},
number = {4},
note = {To appear also in proc. ICALP 2001 Workshop on Verification of Parameterized Systems (VEPAS'01)}
}
@Misc{aee-test-conf-2001,
author = {J\'eron, Thierry},
title = {Le test de conformit\'e~: \'etat de l'art},
howpublished = {Rapport pour l'AEE (Architecture Electronique Embarqu\'ee)},
year = {2001},
url = {http://www.irisa.fr/vertecs/Publis/Ps/2001-AEE_test.ps.gz}
}