Abstractions booléennes pour la vérification des systèmes temps-réel, Tools supported real-time system verification with combination of abstraction/deduction and Model checking

Eun-Young Kang

Description

Sous la direction de Stephan Merz
Thèse soutenue le 08 novembre 2007: Nancy 1
Cette thèse présente un schéma formel et efficace pour la vérification de systèmes temps-réel. Ce schéma repose sur la combinaison par abstraction de techniques déductives et de model checking, et cette combinaison permet de contourner les limites de chacune de ces techniques. La méthode utilise le raffinement itératif abstrait (IAR) pour le calcul d'abstractions finies. Etant donné un système de transitions et un ensemble fini de prédicats, la méthode détermine une abstraction booléenne dont les états correspondent à des ensembles de prédicats. La correction de l'abstraction par rapport au système d'origine est garantie en établissant un ensemble de conditions de vérification, issues de la procédure IAR. Ces conditions sont à démontrer à l'aide d'un prouveur de théorèmes. Les propriétés de sûreté et de vivacité sont ensuite vérifiées par rapport au modèle abstrait. La procédure IAR termine lorsque toutes les conditions sont vérifiées. Dans le cas contraire, une analyse plus fine détermine si le modèle abstrait doit être affiné en considérant davantage de prédicats. Nous identifions une classe de diagrammes de prédicats appelés PDT (predicate diagram for timed system) qui décrivent l'abstraction et qui peuvent être utilisés pour la vérification de systèmes temporisés et paramétrés.
-Model checking
This thesis provides an efficient formal scheme for the tool-supported real-time system verification by combination of abstraction-based deductive and model checking techniques in order to handle the limitations of the applied verification techniques. This method is based on IAR (Iterative Abstract Refinement) to compute finite state abstractions. Given a transition system and a finite set of predicates, this method determines a finite abstraction, where each state of the abstract state space is a true assignment to the abstraction predicates. A theorem prover can be used to verify that the finite abstract model is a correct abstraction of a given system by checking conformance between an abstract and a concrete model by establishing/proving that a set of verification conditions are obtained during the IAR procedure. Then the safety/liveness properties are checked over the abstract model. If the verification condition holds successfully, IAR terminates its procedure. Otherwise more analysis is applied to identify if the abstract model needs to be more precise by adding extra predicates. As abstraction form, we adopt a class of predicate diagrams and define a variant of predicate diagram PDT (Predicate Diagram for Timed systems) that can be used to verify real-time and parameterized systems.
Source: http://www.theses.fr/2007NAN10089/document

Sujets

• Model checking

Informations

• Publié par: Thesee
• Nombre de lectures: 33
• Langue: English

Extrait

AVERTISSEMENT

Ce document est le fruit d'un long travail approuvé par le
jury de soutenance et mis à disposition de l'ensemble de la
communauté universitaire élargie.

Il est soumis à la propriété intellectuelle de l'auteur. Ceci
implique une obligation de citation et de référencement lors
de l’utilisation de ce document.

Toute contrefaçon, plagiat, reproduction illicite encourt une
poursuite pénale.


➢ Contact SCD Nancy 1 : [e-mail]




LIENS


Code de la Propriété Intellectuelle. articles L 122. 4
Code de la Propriété Intellectuelle. articles L 335.2- L 335.10
http://www.cfcopies.com/V2/leg/leg_droi.php
http://www.culture.gouv.fr/culture/infos-pratiques/droits/protection.htm ´D´epartement de formation doctorale en informatique Ecole doctorale IAEM Lorraine
UFR STMIA
Abstractions bool´eennes pour la
v´erification des syst`emes temps-r´eel
`THESE
pr´esent´ee et soutenue publiquement le 8 Novembre 2007
pour l’obtention du
Doctorat de l’universit´e Henri Poincar´e – Nancy 1
(sp´ecialit´e informatique)
par
Eun-Young Kang
Composition du jury
Rapporteurs : Christian Attiogb´e Maˆıtre de conf´erence
Jean-Paul Bahsoun Prof. Universit´e Paul Sabatier France
Examinateurs : Jean-Paul BODEVEIX Prof. Universit´e Paul Sabatier France
Isabelle CHRISMENT Prof. UHP Nancy 1 France
Yamine AIT-AMEUR Prof. LISI-ENSMA France
´Dominique MERY Prof. UHP Nancy 1 France
Stephan MERZ Directeur de recherche INRIA France
Laboratoire Lorrain de Recherche en Informatique et ses Applications — UMR 7503o
la
ve
i
t
s
.
e

n

p
hl
a
ria
ge
M
aAbstract
This thesis provides an efficient formal scheme for the tool-supported real-time
system verification by combination of abstraction-based deductive and model
checking techniques in order to handle the limitations of the applied verifica-
tion techniques. This method is based on IAR (Iterative Abstract Refinement)
to compute finite state abstractions. Given a transition system and a finite set
of predicates, this method determines a finite abstraction, where each state of
the abstract state space is a true assignment to the abstraction predicates. A
theorem prover can be used to verify that the finite abstract model is a correct
abstraction of a given system by checking conformance between an abstract and
a concrete model by establishing/proving that a set of verification conditions
are obtained during the IAR procedure. Then the safety/liveness properties are
checked over the abstract model. If the verification condition holds successfully,
IAR terminates its procedure. Otherwise more analysis is applied to identify
if the abstract model needs to be more precise by adding extra predicates. As
abstraction form, we adopt a class of predicate diagrams and define a variant
of predicate diagram PDT (Predicate Diagram for Timed systems) that can be
used to verify real-time and parameterized systems.
Key words : Real-time system verification, model checking, deduc-
tive technique, and predicate abstraction
R´esum´e
Cetteth`esepr´esenteunsch´emaformeletefficacepourlav´erificationdesyst`emes
temps-r´eel. Ce sch´ema repose sur la combinaison par abstraction de techniques
d´eductives et de model checking, et cette combinaison permet de contourner les
limites de chacune de ces techniques. La m´ethode utilise le raffinement it´eratif
abstrait (IAR) pour le calcul d’abstractions finies. Etant donn´e un syst`eme de
transitions et un ensemble fini de pr´edicats, la m´ethode d´etermine une abstrac-
tion bool´eenne dont les ´etats correspondent a` des ensembles de pr´edicats. La
correction de l’abstraction par rapport au syst`eme d’origine est garantie en
´etablissant un ensemble de conditions de v´erification, issues de la proc´edure
IAR. Ces conditions sont `a d´emontrer a` l’aide d’un prouveur de th´eor`emes. Les
propri´et´es de suretˆ ´e et de vivacit´e sont ensuite v´erifi´ees par rapport au mod`ele
abstrait. La proc´edure IAR termine lorsque toutes les conditions sont v´erifi´ees.
Dans le cas contraire, une analyse plus fine d´etermine si le mod`ele abstrait doit
ˆetre affin´e en consid´erant davantage de pr´edicats. Nous identifions une classe
de diagrammes de pr´edicats appel´es PDT (predicate diagram for timed system)
qui d´ecrivent l’abstraction et qui peuvent ˆetre utilis´es pour la v´erification de
syst`emes temporis´es et param´etr´es.
Mots cl´es : v´erification de syst`emes temps-r´eel, model checking, tech-
nique d´eductive, et pr´edicats d’abstractionAbstract
Modelcheckinghasbeenbroadlyconsideredandusefulinverificationforfinite
state real time systems. Theoritically optimal algorithms make model checking
successful in a way that a system and a property to check and automatically
either proves it correct or comes up with a violation. Unfortunately, although
these algorithms are fully automatic, they are confronted with a state explosion
problem. They are typically exponential in the number and maximum values of
clocks.
On the other hand, deductive techniques can in principle be used to verify
infinite, or unbounded systems and also large finite state systems, based on suit-
able sets of axioms and inference rules. Although they are supported by theorem
provers and interactive proof assistants, their use requires considerable expertise
and tedious/repetitive user interaction.
Predicate abstraction provides a different approach to computing finite state
abstractions. Given a transition system abd a finite set of predicates, this method
determines a finite abstraction, where each state of the abstract state space is a
true assignment to the abstraction predicates.
Model checking and abstraction/deductive techniques are therefore comple-
mentary.Thuswehaveproposedanefficientschemebycombinationofabstraction-
baseddeductiveandmodelcheckingtechniquesthatshouldgivearisetopowerful
verification environment. This method is based on our IAR (Iterative Abstract
Refinement) algorithm to provide a formal framework for verifying a rich class or
safety and liveness properties of timed systems.
IAR computes an abstract model and a theorem prover can be used to verify
thatthefiniteabstractmodelisacorrectabstractionofagivensystembychecking
conformance between an abstract and a concrete model by establishing/proving
that a set of verification conditions are obtained during the IAR procedure. Then
the safety/liveness properties are checked over the abstract model. If the verifica-
tion condition holds successfully, IAR terminates its procedure. Otherwise more
iii ABSTRACT
analysis is applied to identify if the abstract model needs to be more precise by
adding extra predicates.
As abstraction form, we adopt a class of predicate diagrams and define a
variant of predicate diagram PDT (Predicate Diagram for Timed systems) that
can be used to verify real-time and parameterized systems.
Eun-Young KangAcknowledgements
The road has been rather long — not to mention somewhat winding.
Overtheyearsithasbeenmygoodfortunetoencountermanypeoplewhohave
given me their time, companionship, professional and personal help, and above
all, their patience. This was certainly more than was warranted by my seeming
determinationtoindefinitelypositionthedeadlineforfinishingthisthesisat“this
year”.
Iwouldfirstofallliketothankmymentor,StephanMerz.Henotonlygaveme
thescientificsupportandsupervisionthatagraduatestudentcanexpectfromhis
professionalresearch,buthealsoallowedandencouragedmetocontinuemyPh.D
work as part of “Cotutelle”, in the MOSEL group at LORIA after I had formally
left the Netherlands. My sincere thanks to him : I could not have wished for a
more thorough discussion partner and sounding board (on any subject under the
sun).Duringthehardestdaysofmyresearchhisamazingknowledge(particularly
with respect on logics and formal methods) has been an excellent guiding light,
helpingthemethodologydescribedinthisthesistocometolife.Withouthisgreat
supporting, I would never have made it this far.
HansToetenel,thenofDelftUniversityinHolland,wasmyprimarysupervisor
in the early years. His ideas, his research, and especially his unique brand of
enthusiasmformthemodelcheckingonwhichmuchofthisthesisisbuilt.Icannot
help but feel apologetic towards him over the fact that the specification language
— so very much a cornerstone of our work in those early days — eventually fell
by the wayside...
There are five fellow researchers whom I would specifically like to thank for
the support they have given me over the years : Ronald Lutje Spelberg for his
work on the specification notation with formal semantics of XTGs, Dominique
Cansell, Dominique Mery and Stephan Merz for the early work on the definition
and semantics of predicate diagrams, and Loic Fejoz for his implementation of
iiiiv ACKNOWLEDGEMENTS
predicate diagrams in the DIXIT toolkit.