Markey-these-slides

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 ...

Informations

• Publié par: Esli
• Nombre de lectures: 10
• Langue: English

Extrait

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