The SPIN verification system : the second Workshop on the SPIN Verification System : proceedings of a DIMACS workshop, August 5, 1996
著者
書誌事項
The SPIN verification system : the second Workshop on the SPIN Verification System : proceedings of a DIMACS workshop, August 5, 1996
（DIMACS series in discrete mathematics and theoretical computer science, v. 32）
American Mathematical Society, c1997
大学図書館所蔵 件 / 全9件
-
該当する所蔵館はありません
- すべての絞り込み条件を解除する
注記
Workshop held at Rutgers Univ. in New Brunswick, N.J
Includes bibliographical references
内容説明・目次
内容説明
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.
目次
State space compression with graph encoded sets by J.-C. Gregoire Not checking for closure under stuttering by G. J. Holzmann and O. Kupferman On nested depth first search by G. J. Holzmann, D. Peled, and M. Yannakakis Modelling and analysis of a collision avoidance protocol using Spin and Uppaal by H. E. Jensen, K. G. Larsen, and A. Skou The application of Promela and Spin in the BOS project by P. Kars Implementing and verifying MSC specifications using Promela/XSpin by S. Leue and P. B. Ladkin Creating implementations from Promela models by S. Loffler and A. Serhrouchni Modelling and verification of the MCS layer with Spin by P. Merino and J.-M. Troya Protocol verification with reactive Promela/Rspin by E. Najm and F. Olsen Outline for an operational semantics of Promela by V. Natarajan and G. J. Holzmann A simulation and validation tool for self-stabilizing protocols by S. K. Shukla, D. J. Rosenkrantz, and S. S. Ravi Dynamic analysis of SA/RT models using Spin and modular verification by J. Tuya, J. R. de Diego, C. de la Riva, and J. A. Corrales Memory efficient state storage in Spin by W. Visser and H. Barringer.
「Nielsen BookData」 より
