Paper Info
Title
A generalized semantics of PROMELA for abstract model checking
Abstract
Semantics of description languages for complex systems are a central issue for implementing verification methods such as abstract model checking. This technique is employed to verify systems by inspecting only a small state space that represents its potential behaviors. This paper presents a generalized operational semantics of the modelling language promela that provides the theoretical basis to introduce this promising method in the model checker SPIN. The generalization consists of identifying language aspects affected by the abstraction. Using these aspects as parameters, it is possible to obtain and relate different interpretations of the language. The new semantics provides a framework to reason about how to construct the tool αspin as an extension of spin.
Year
DOI
Venue
2004
10.1007/s00165-004-0040-y
Formal Asp. Comput.
Keywords
Field
DocType
Model checking,Abstraction,Structured operational semantics,promela,spin
Complex system,Operational semantics,Model checking,Computer science,Computational semantics,Denotational semantics,Theoretical computer science,Promela,State space,Semantics
Journal
Volume
Issue
ISSN
16
3
0934-5043
Citations 
PageRank 
References 
13
0.72
22
Authors
3
Name
Order
Citations
PageRank
María del Mar Gallardo114113.16
Pedro Merino220125.98
Ernesto Pimentel351542.20