27 Pages



Downloading requires you to have access to the YouScribe library
Learn all about the services we offer


ƒƒƒƒƒƒƒ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: email: Array bounds violationsFortunately, most of these 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 ...



Published by
Reads 12
Language English
(X)Spin Archite