Markey-these-slides

Markey-these-slides

Documents
77 pages
Lire
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Description

Logiques temporelles pour la vérification :expressivité, complexité, algorithmesSoutenance de Thèse – 03 avril 2003Nicolas MARKEYLaboratoire d’Informatique Fondamentale d’OrléansFormal verification? Back• Why is verification crucial?− Reactive systems are everywhere,− They are ever more complex,− Numerous bugs have occurred (Ariane V, Therac-25, ...)Formal verification? Back• Why is verification crucial?− Reactive systems are everywhere,− They are ever more complex,− Numerous bugs have occurred (Ariane V, Therac-25, ...)• Strict methods are necessary for verifying or certifying systems.Formal verification? Back• Why is verification crucial?− Reactive systems are everywhere,− They are ever more complex,− Numerous bugs have occurred (Ariane V, Therac-25, ...)• Strict methods are necessary for verifying or certifying systems.• Possible methods for formal verification:− Formal proof,− Testing,− Model checking...Verification by model checking Back?System PropertysatisfiesVerification by model checking Back?System PropertysatisfiesModel CheckerVerification by model checking Back?System Propertysatisfiesmodel of the SystemModel CheckerVerification by model checking Back?System Propertysatisfiesmodel of the System Formula expressing the PropertyModel CheckerVerification by model checking Back?System Propertysatisfiesmodel of the System Formula expressing the PropertyModel CheckerVerification by model checking Back?System ...

Sujets

Informations

Publié par
Nombre de visites sur la page 10
Langue English
Signaler un problème
Logiques temporelles pour la vérification expressivité, complexité, algorithmes
Soutenance de Thèse – 03 avril 2003
Nicolas M
ARKEY
Laboratoire d’Informatique Fondamentale d’Orléans
:
Formal verification?
Why is verificationcrucial?
Reactive systems areeverywhere,
They are ever morecomplex,
Numerous
bugs
have
occurred
(Ariane
V,
Therac-25,
...)
Bakc
Formal verification?
Why is verificationcrucial? Reactive systems areeverywhere, They are ever morecomplex, Numerousbugshave occurred (Ariane V, Therac-25, ...)
Strict methods are necessary for verifying or certifying systems.
aBkc
Formal verification?
Why is verificationcrucial? Reactive systems areeverywhere, They are ever morecomplex, Numerousbugshave occurred (Ariane V, Therac-25, ...)
Strict methods are necessary for verifying or certifying systems.
formal verification:
Possible methods for Formal proof, Testing, Model checking...
aBkc
Verification
System
by
model
?
satisfies
checking
Property
aBkc
Verification
System
by
model
? satisfies
Model
checking
Checker
Property
Back
Verification
System
by
model of theSystem
model
? satisfies
checking
Model Checker
Property
aBkc
Verification by
System
model of theSystem
model checking
? satisfies
Property
Formula expressing theProperty
Model Checker
Back
Verification by
System
model of theSystem
model checking
? satisfies
Property
Formula expressing theProperty
Model Checker
Bakc
Property
? satisfies
model of theSystem
System
Model Checker
Formula expressing theProperty
yes/no
model checking
Verification by
kcaB
Kripke
We
use
Kripke
structures
structures
for
mo
delling
the
system.
Back