Skip to main content
SpringerLink
Log in

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

  • Conference proceedings
  • © 1999

Overview

Editors:
  1. Dennis Dams

    1. Department of Electrical Engineering and Department of Mathematics and Computer Science, Eindhoven University of Technology, MB Eindhoven, The Netherlands

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Rob Gerth

    1. Intel Microprocessor Products Group, Strategic CAD Laboratories, Hillsboro, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Stefan Leue

    1. Department of Electrical and Computer Engineering, University of Waterloo, Waterloo, Canada

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  4. Mieke Massink

    1. C.N.R.-Ist., Pisa, Italy

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 1680)

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (20 papers)

  1. Part II: Papers Presented at 6thSPIN99

    1. Extensions

      1. dSPIN: A Dynamic Extension of SPIN
        • Claudio Demartini, Radu Iosif, Riccardo Sisto
        Pages 261-276

  2. Back Matter

    Pages 277-277
    Download chapter PDF
Back to top

Keywords

About this book

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

Editors and Affiliations

  • Department of Electrical Engineering and Department of Mathematics and Computer Science, Eindhoven University of Technology, MB Eindhoven, The Netherlands

    Dennis Dams

  • Intel Microprocessor Products Group, Strategic CAD Laboratories, Hillsboro, USA

    Rob Gerth

  • Department of Electrical and Computer Engineering, University of Waterloo, Waterloo, Canada

    Stefan Leue

  • C.N.R.-Ist., Pisa, Italy

    Mieke Massink

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation