The Spin Verification System: Dimacs Workshop, August 5, 1996 (Dimacs Series in Discrete Mathematics and Theoretical Computer Science)

Workshop, on the Spin Verification), Jean-Charles Gregoire and Gerard J. Holzmann

ISBN 10: 0821806807 / ISBN 13: 9780821806807

Verlag: Oxford University Press 01.06.1997., 1997

Beschreibung

203 Seiten ex Library Book aus einer wissenschafltichen Bibliothek Sprache: Englisch Gewicht in Gramm: 969 26,0 x 18,4 x 1,6 cm, Gebundene Ausgabe.

Bestandsnummer des Verkäufers 370890

Bibliografische Details

• Titel: The Spin Verification System: Dimacs Workshop, August 5, 1996 (Dimacs Series in Discrete Mathematics and Theoretical Computer Science)
• Verlag: Oxford University Press 01.06.1997.
• Erscheinungsjahr: 1997
• Sprache: Englisch
• ISBN-10: 0821806807
• ISBN-13: 9780821806807
• Einband: Hardcover
• Zustand: Sehr gut
• Verkäuferkataloge:
  • Alle Bücher

Über diesen Titel

Inhaltsangabe

What is Spin? Spin is a general tool for the specification and formal verification of software for distributed systems. It has been used to detect design errors in a wide range of applications, such as abstract distributed algorithms, data communications protocols, operating systems code, and telephone switching code. The verifier can check for basic correctness properties, such as absence of deadlock and race conditions, logical completeness, or unwarranted assumptions about the relative speeds of correctness properties expressed in the syntax of Linear-time Temporal Logic (LTL). The tool translates LTL formulae automatically into automata representations, which can be used in an efficient on-the-fly verifications procedure.This DIMACS volume presents the papers contributed to the second international workshop that was held on the Spin verification system at Rutgers University in August 1996. The work covers theoretical and foundational studies of formal verification, empirical studies of the effectiveness of different types of algorithms, significant practical applications of the Spin verifier, and discussions of extensions and revisions of the basic code.

Reseña del editor

What is SPIN? SPIN is a general tool for the specification and formal verification of software for distributed systems. It has been used to detect design errors in a wide range of applications, such as abstract distributed algorithms, data communications protocols, operating systems code, and telephone switching code. The verifier can check for basic correctness properties, such as absence of deadlock and race conditions, logical completeness, or unwarranted assumptions about the relative speeds of processes. It can also check for more subtle, system dependent correctness properties expressed inthe syntax of Linear-time Temporal Logic (LTL). The tool translates LTL formulae automatically into automata representations, which can be used in an efficient on-th-fly verifications procedure. This DIMACS volume presents the papers contributed to the second international workshop that was held on the SPIN verification system at Rutgers University in August 1996. The work covers theoretical and foundational studies of formal verifications, empirical studies of the effectiveness of different types of algorithms, significant practical applications of the SPIN verifier, and discussions of extensions and revisions of the basic code. This text will be of interest to those working in applications.