Theoretical and Practical Aspects of SPIN Model Checking 5th and 6th International SPIN Workshops, Trento, Italy, July 5, 1999, Toulouse, France, September 21 and 24, 1999, Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Dams, Dennis (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Gerth, Robert (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Leue, Stefan (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Massinek, Mieke (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1999.
• Έκδοση: 1st ed. 1999.
• Σειρά: Lecture Notes in Computer Science, 1680
• Θέματα: Computer software.; Computer logic.; Software engineering.; Programming languages (Electronic computers).; Mathematical Software.; Logics and Meanings of Programs.; Software Engineering.; Programming Languages, Compilers, Interpreters.

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

Πίνακας περιεχομένων:

• I: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.