Early model checkers considered finite-state systems described by boolean variables, and did not support an explicit modeling of time. This approach is inadequate for embedded systems whose correct functioning depends crucially on timing delays and continuous parameters. Since we proved that algorithmic analysis is possible even in presence continuously-evolving clock variables, real-time model checking has witnessed extensive research. I will survey the progress in specification and analysis of embedded systems by discussing theoretical results, tools, and case-studies.
The second problem concerns a recent proposal for model checking of open systems. The evolution of an open system can be viewed as a game between the system and its environment. As a specification language, we propose "alternating-time" temporal logic that allows a natural expression of game-like properties that are not expressible in the commonly-used logic CTL. I will discuss the motivations behind this reformulation of the model checking problem, and present a symbolic fixpoint computation procedure to solve it.
|
Modified: Jun 24, 1997|
Current events|
Your comments
and inquiries are welcome.