fm2003-adv-spin-tutorial
27 Pages
English

fm2003-adv-spin-tutorial

-

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

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: gholzmann@acm.org email: ruys@cs.utwente.nl 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 ...

Subjects

Informations

Published by
Reads 12
Language English
(X)Spin Archite
re