000 05089nam a22006135i 4500
001 978-3-540-48234-5
003 DE-He213
005 20240423132434.0
007 cr nn 008mamaa
008 121227s1999 gw | s |||| 0|eng d
020 _a9783540482345
_9978-3-540-48234-5
024 7 _a10.1007/3-540-48234-2
_2doi
050 4 _aQA76.75-76.765
072 7 _aUFM
_2bicssc
072 7 _aCOM077000
_2bisacsh
072 7 _aUFM
_2thema
082 0 4 _a510.285
_223
245 1 0 _aTheoretical and Practical Aspects of SPIN Model Checking
_h[electronic resource] :
_b5th and 6th International SPIN Workshops, Trento, Italy, July 5, 1999, Toulouse, France, September 21 and 24, 1999, Proceedings /
_cedited by Dennis Dams, Robert Gerth, Stefan Leue, Mieke Massinek.
250 _a1st ed. 1999.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c1999.
300 _aX, 282 p.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Computer Science,
_x1611-3349 ;
_v1680
505 0 _aI:Selection of Papers Presented at 5thSPIN99 -- Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving -- Runtime Efficient State Compaction in Spin -- Distributed-Memory Model Checking with SPIN -- Partial Order Reduction in Presence of Rendez-vous Communications with Unless Constructs and Weak Fairness -- Divide, Abstract, and Model-Check -- II: Papers Presented at 6thSPIN99 -- Formal Methods Adoption: What’s Working, What’s Not! -- Model Checking for Managers -- Xspin/Project - Integrated Validation Management for Xspin -- Analyzing Mode Confusion via Model Checking -- Detecting Feature Interactions in the Terrestrial Trunked Radio (TETRA) Network Using Promela and Xspin -- Java PathFinder A Translator from Java to Promela -- VIP: A Visual Interface for Promela -- Events in Property Patterns -- Assume-Guarantee Model Checking of Software: A Comparative Case Study -- A Framework for Automatic Construction of Abstract Promela Models -- Model Checking Operator Procedures -- Applying Model Checking in Java Verification -- The Engineering of a Model Checker: the Gnu i-Protocol Case Study Revisited. -- Embedding a Dialect of SDL in PROMELA -- dSPIN: A Dynamic Extension of SPIN.
520 _aIncreasing the designer’s con dence that a piece of software or hardwareis c- pliant with its speci cation has become a key objective in the design process for software and hardware systems. Many approaches to reaching this goal have been developed, including rigorous speci cation, formal veri cation, automated validation, and testing. Finite-state model checking, as it is supported by the explicit-state model checkerSPIN,is enjoying a constantly increasingpopularity in automated property validation of concurrent, message based systems. SPIN has been in large parts implemented and is being maintained by Gerard Ho- mann, and is freely available via ftp fromnetlib.bell-labs.comor from URL http://cm.bell-labs.com/cm/cs/what/spin/Man/README.html. The beauty of nite-state model checking lies in the possibility of building \push-button" validation tools. When the state space is nite, the state-space traversal will eventually terminate with a de nite verdict on the property that is being validated. Equally helpful is the fact that in case the property is inv- idated the model checker will return a counterexample, a feature that greatly facilitates fault identi cation. On the downside, the time it takes to obtain a verdict may be very long if the state space is large and the type of properties that can be validated is restricted to a logic of rather limited expressiveness.
650 0 _aComputer software.
650 0 _aComputer science.
650 0 _aSoftware engineering.
650 0 _aCompilers (Computer programs).
650 1 4 _aMathematical Software.
650 2 4 _aComputer Science Logic and Foundations of Programming.
650 2 4 _aSoftware Engineering.
650 2 4 _aCompilers and Interpreters.
700 1 _aDams, Dennis.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aGerth, Robert.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aLeue, Stefan.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aMassinek, Mieke.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783540664994
776 0 8 _iPrinted edition:
_z9783662211687
830 0 _aLecture Notes in Computer Science,
_x1611-3349 ;
_v1680
856 4 0 _uhttps://doi.org/10.1007/3-540-48234-2
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
912 _aZDB-2-BAE
942 _cSPRINGER
999 _c187752
_d187752