Paper Info
Title
Discrete-Time Promela and Spin
Abstract
Spin is software package for verification of concurrent systems. The formal models of the systems that are verified, are built in Promela - Spin's input language. We present an extension of Promela and Spin with discrete time that provides an opportunity to model systems which correct functioning crucially de- pends on timing parameters. The new version of the tool is completely compatible with all the features the standard package, including partial order reduction. We have tested the prototype tool on several applications known in the verification literature and the first results are very promising. The Spin Model Checker. Originally, Promela and Spin have been developed for analy- sis and validation of communication protocols (10). The language syntax is derived form C, but also uses the denotations for communications from Hoare's CSP and control flow statements based on Dijkstra's guarded commands. The full presentation of Promela and Spin is beyond the scope of this paper and we suggest (10) as a reference to the inter- ested reader. Following (11) we only give a short overview of the language and validation tools. In Promela, the system components are modeled as processes that can communi- cate via channels either by buffered message exchanges or rendez-vous operations, and also trough shared memory represented as global variables. The execution of actions is considered asynchronous and interleaved, which means that in every step only one en- abled action is performed and without any additional assumptions of the relative speed of the process execution. Given as an input a Promela model Spin can do random or interactive simulations or to generate a C program that performs a validation of the system by scanning the state space. The validation with the compiled C program is done in separate phases. The one phase is validation of the safety properties (absence of deadlock, unspecified message receptions, invalid end states and assertions) trough a search of the state space. Verifi- cation of most of the liveness properties can be handled by detection of progress and acceptance cycles. The never-claims constructs are the most general way to verify the system by providing the possibility to express properties as linear-time temporal logic (LTL) formulae. All kinds of errors are reported by saving the trace of the actions leading to an invalid state or cycle. The erroneous sequence can be repeated as a guided simula- tion. The simplest way to do scanning of the state space is trough an exhaustive search. On leave from the Insitiute of Informatics, Faculty of Natural Sciences and Mathematics, Uni- versity "Sts. Cyril and Methodius", Skopje, Macedonia. Supported by EC ESPRIT LTR Project No. 23498 (VIRES). Supported by the Netherlands Computer Science Research Foundation (SION).
Year
DOI
Venue
1998
10.1007/BFb0055359
FTRTFT
Keywords
Field
DocType
discrete-time promela,exhaustive search,discrete time,partial order reduction,control flow,communication protocol,shared memory,state space
Spin-½,Computer science,Algorithm,Real-time operating system,Software,Promela,Discrete time and continuous time,Partial order reduction,Hybrid system,Formal verification
Conference
Volume
ISSN
ISBN
1486
0302-9743
3-540-65003-2
Citations 
PageRank 
References 
18
1.09
13
Authors
2
Name
Order
Citations
PageRank
Dragan Bosnacki127626.95
dennis dams21377.90