PhD defense
Florent Bouchy
Thesis title
Logics and models for the verification of infinite systems
-->
slides
Time and place
Tuesday, November 10th, 2009 at 11h00
ATTENTION: strike on RER lines A and B from Monday 9th until...?
Salle de Conférences du Pavillon des Jardins
École Normale Supérieure de Cachan
Plan d'accès
Jury
Abstract
Our current society heavily relies on computer systems: medical devices, public transit, cars, cellphones, nuclear plants, elevators, banks, industry, spatial exploration, etc. These systems are becoming more and more important to our daily life, directly or not. The correct performance of such systems is a major stake on an economical level, as well as on both environmental and human levels. These systems are getting more and more complex due to their sophistication and omnipresence, so much that current engineering techniques are generally unable to guarantee that the systems surrounding us are operating correctly.
The model-checking technique relies on the modelling of such systems (namely using finite automata, possibly extended with variables, stacks, channels, etc.), and on the modelling of properties ensuring correct operation of systems (using temporal logics). The complexity of current systems suggests the application of model-checking techniques to infinite-state systems, in particular by endowing automata with the ability to use unbounded variables so that the models get closer to reality. Considered variables are either real-valued, integer-valued, or mixed (i.e. both at the same time).
In order to represent infinite sets of values for such variables, we use first-order arithmetical logics. We introduce a means to decomposing real-valued or mixed logics into integer-valued logics and decimal logics (i.e. real-valued between 0 and 1). We also define a decidable mixed logic which has a greater expression power than most known first-order logics.
We study models for infinite-state systems extended with time, counting, or both at the same time. We then look into their reachability problems, i.e. knowing whether for a given model, the set of its reachable configurations is computable. We define a new model for timed counter systems, for which we generalize the region graph construction, enabling to decide rechability problems according to the expression power of counters. Finally, we complete the study of DCM (a model introduced by Ibarra and San Pietro) by generalizing the guards allowed on transitions, by bringing new decidability results, and by showing that every formula of the mixed linear arithmetic is definable by a reversal-bounded DCM.
Keywords
Formal verification, Mathematical logic, Systems models, Automata
Go to Florent Bouchy's
web page