Notice bibliographique
- Notice
Type(s) de contenu et mode(s) de consultation : Texte noté : électronique
Auteur(s) : Ben-Ari, Mordechai (1948-....)
Titre(s) : Principles of the Spin model checker [Texte électronique] / Mordechai Ben-Ari
Publication : London : Springer, cop. 2008
Description matérielle : 1 ressource dématérialisée
Note(s) : Includes bibliographical references (pages 209-210) and index
The Spin model checker is a widely used professional software tool for specifying
and verifying concurrent and distributed systems. Models, written in a simple language
called Promela, can be simulated randomly or interactively. Spin can generate efficient
verifiers that search for a counterexample to correctness specifications applied to
a model. Spin is also a superb tool for teaching important concepts of computer science
such as verification, concurrency and nondeterminism. The Promela language is easy
to learn, as is the linear temporal logic used for correctness specifications, and
the techniques for simulating and verifying models. Principles of Spin is an introductory
book for students and practicing software engineers who wish to learn Promela and
Spin. The presentation starts with the verification of sequential programs and proceeds
in gradual stages to the verification of concurrent and then distributed programs.
Complete programs are used to demonstrate each construct and concept, and the source
code of these programs, together with that of longer case studies, are available on
the companion website. The book describes free software that the author has developed:
jSpinâan integrated development environment for Spin, SpinSpiderâa visualization tool
that automatically constructs graphical state diagrams of concurrent programs, and
VNâa Spin-based tool for visualizing nondeterminism of finite automata. -- From the
Back Cover
Sujet(s) : Protocoles de réseaux d'ordinateurs
Algorithmes
Indice(s) Dewey :
005.14 (23e éd.) = Programmation (informatique) - Vérification, tests, mesures, débogage
Identifiants, prix et caractéristiques : ISBN 9781846287701
Identifiant de la notice : ark:/12148/cb446704567
Notice n° :
FRBNF44670456
(notice reprise d'un réservoir extérieur)
Table des matières : 1 ; Sequential Programming in Promela11.1 ; A first program in Promela11.2 ; Random
simulation21.3 ; Data types41.3.1 ; Type conversions61.4 ; Operators and expressions61.4.1
; Local variables71.4.2 ; Symbolic names81.5 ; Control statements101.6 ; Selection
statements101.6.1 ; Conditional expressions141.7 ; Repetitive statements151.7.1 ;
Counting loops161.8 ; Jump statements172 ; Verification of Sequential Programs192.1
; Assertions192.2 ; Verifying a program in Spin232.2.1 ; Guided simulation262.2.2
; Displaying a computation263 ; Concurrency293.1 ; Interleaving293.1.1 ; Displaying
a computation313.2 ; Atomicity333.3 ; Interactive simulation343.4 ; Interference between
processes353.5 ; Sets of processes373.6 ; Interference revisited383.7 ; Deterministic
sequences of statements403.8 ; Verification with assertions423.9 ; The critical section
problem444 ; Synchronization474.1 ; Synchronization by blocking474.2 ; Executability
of statements504.3 ; State transition diagrams514.4 ; Atomic sequences of statements544.4.1
;
