Paper Info
Title
Formal Verification of Statecharts with Instantaneous Chain Reaction
Abstract
We present a method for symbolic model checking of mu-Charts, a Statecharts dialect with instantaneous broadcast communication. Due to this communication concept, mu-Charts satisfy the perfect synchrony hypothesis. The well-known causality conflicts that arise under instantaneous feedback from negative trigger conditions are resolved semantically through oracle signals. We have implemented a prototypical tool that translates mu-Charts specifications into mu-calculus formulae. These formulae are checked against temporal specifications using a mu-calculus verifier.
Year
DOI
Venue
1997
10.1007/BFb0035391
TACAS
Keywords
Field
DocType
instantaneous chain reaction,formal verification
Causality,Model checking,Computer science,Oracle,Theoretical computer science,Broadcast communication network,Formal verification
Conference
Volume
ISSN
ISBN
1217
0302-9743
3-540-62790-1
Citations 
PageRank 
References 
8
0.76
12
Authors
2
Name
Order
Citations
PageRank
Jan Philipps116216.45
Peter Scholz215513.69