Sciweavers

Share
ICSE
2001
IEEE-ACM

JMOCHA: A Model Checking Tool that Exploits Design Structure

9 years 4 months ago
JMOCHA: A Model Checking Tool that Exploits Design Structure
Mocha is a model checker based on the theme of exploiting design modularity: instead of manipulating unstructured state-transition graphs, it supports the hierarchical modeling framework of Reactive Modules. The hierarchy is exploited by the tool in three ways. First, veri cation tasks such as re nement checking can be decomposed into subgoals using assume-guarantee rules. Second, instead of traditional temporal logics such as CTL, Mocha supports Alternating Temporal Logic (ATL), a game-based temporal logic for specifying collaborative as well as adversarial interactions between the components of a design. Third, the search algorithms incorporate optimizations based on the hierarchical reduction of sequences of internal transitions. This report describes a new release, called jMocha, which is implemented in Java and supports many new features, including an extensive GUI and a scripting languages for the rapid prototyping of veri cation algorithms. An abbreviated version of this paper a...
Rajeev Alur, Luca de Alfaro, Radu Grosu, Thomas A.
Added 30 Jul 2010
Updated 30 Jul 2010
Type Conference
Year 2001
Where ICSE
Authors Rajeev Alur, Luca de Alfaro, Radu Grosu, Thomas A. Henzinger, M. Kang, Christoph M. Kirsch, Rupak Majumdar, Freddy Y. C. Mang, Bow-Yaw Wang
Comments (0)
books