fm2003-adv-spin-tutorial

Ruys

Description

ƒƒƒƒƒƒƒversion: 8 September 2003FM 2003, Pisa, Italy, 8 September 2003Common Design Flaws• DeadlockAdvanced In designing distributed systems:network applications, • Livelock, starvationdata communication protocols, SPIN Tutorial multithreaded code, • Underspecificationclient-server applications.unexpected reception of messages• OverspecificationDesigning concurrent (software) Gerard Holzmann Theo RuysDead codesystems is so hard, that these flaws are mostly overlooked...NASA/JPL Laboratory for University of Twente• Violations of constraintsReliable Software The NetherlandsPasadena, CA Buffer overrunsemail: [e-mail] email: [e-mail] Array bounds violationsFortunately, most of these http://spinroot.com/gerard http://www.cs.utwente.nl/~ruys/design errors can be detected• Assumptions about speedusing model checking techniques!Logical correctness vs. real-time performanceFM 2003 Tutorial Pisa, Italy, 8 September 2003FM 2003 Gerard Holzmann & Theo Ruys Advanced SPIN Tutorial 2Model Checking Verification vs. DebuggingModelM• Two (extreme) approaches with respect to the application byte n;proctype Aap() {of model checkers.doProperty φ:: n++:: noot!MIESod [] (n<3) verification approach: tries to ascertain the correctness of a }detailed model M of the system under validation.debugging approach: tries to find errors in a model M.State Space• Model checking is most effective in combination with the debugging ...

Informations

• Publié par: Sonab
• Nombre de lectures: 13
• Langue: English

Extrait

(X)Spin Archite

re