Friday, September 24, 1999
1:00 PM
Room NE43-518
Theory of Distributed Systems Seminar
Abstract
Model checking is emerging as a practical tool for detecting errors in early stages of system design, but its application still requires considerable expertise due to well-known limitations of state-space search. Most of the existing tools view model checking as analysis of a flat state-transition graph. Our agenda is to enrich the modeling language with those design constructs that can be analyzed efficiently. Exploiting modularity in the design structure during analysis is a central theme of the model checker MOCHA, a joint project between UC Berkeley and Penn. In this talk, I will first give an overview of MOCHA, give a demo, and then, discuss current research themes which include (1) refinement checking using assume-guarantee reasoning, (2) analysis of hierarchical state machines, and (3) modular reasoning based on solving games.
|
Modified: Sep 22, 1999|
Current events|
Your comments
and inquiries are welcome.