Sciweavers

Share
CAV
2000
Springer

Efficient Reachability Analysis of Hierarchical Reactive Machines

9 years 7 months ago
Efficient Reachability Analysis of Hierarchical Reactive Machines
Hierarchical state machines is a popular visual formalism for software specifications. To apply automated analysis to such specifications, the traditional approach is to compile them to existing model checkers. Aimed at exploiting the modular structure more effectively, our approach is to develop algorithms that work directly on the hierarchical structure. First, we report on an implementation of a visual hierarchical language with modular features such as nested modes, variable scoping, mode reuse, exceptions, group transitions, and history. Then, we identify a variety of heuristics to exploit these modular features during reachability analysis. We report on an enumerative as well as a symbolic checker, and case studies.
Rajeev Alur, Radu Grosu, Michael McDougall
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where CAV
Authors Rajeev Alur, Radu Grosu, Michael McDougall
Comments (0)
books