Paper Info
Title
State/Event software verification for branching-time specifications
Abstract
In the domain of concurrent software verification, there is an evident need for specification formalisms and efficient algorithms to verify branching-time properties that involve both data and communication. We address this problem by defining a new branching-time temporal logic SE-A${\it \Omega}$ which integrates both state-based and action-based properties. SE-A${\it \Omega}$ is universal, i.e., preserved by the simulation relation, and thus amenable to counterexample-guided abstraction refinement. We provide a model-checking algorithm for this logic, based upon a compositional abstraction-refinement loop which exploits the natural decomposition of the concurrent system into its components. The abstraction and refinement steps are performed over each component separately, and only the model checking step requires an explicit composition of the abstracted components. For experimental evaluation, we have integrated our algorithm within the ComFort reasoning framework and used it to verify a piece of industrial robot control software.
Year
DOI
Venue
2005
10.1007/11589976_5
IFM
Keywords
Field
DocType
refinement step,concurrent system,model-checking algorithm,industrial robot control software,branching-time specification,new branching-time temporal logic,counterexample-guided abstraction refinement,comfort reasoning framework,efficient algorithm,concurrent software verification,event software verification,branching-time property,model checking,temporal logic,software verification
Model checking,Programming language,Abstraction,Concurrency,Computer science,Theoretical computer science,Industrial robot,Temporal logic,Formal methods,Rotation formalisms in three dimensions,Software verification
Conference
Volume
ISSN
ISBN
3771
0302-9743
3-540-30492-4
Citations 
PageRank 
References 
15
0.73
22
Authors
7
Name
Order
Citations
PageRank
Sagar Chaki168741.58
Edmund M. Clarke2206452418.32
Orna Grumberg34361351.99
Joël Ouaknine4148199.25
Natasha Sharygina5106868.33
Tayssir Touili675847.21
Helmut Veith72476140.58