Students: Monica Brockmeyer and Elly Winner
Professor: Farnam Jahanian
Collaborators: Connie Heitmeyer and Bruce Labaw, NRL
Sponsor: Naval Research Laboratory
As software control of time-critical functions in embedded systems becomes more common, a means for the precise specification of their behavior and formal methods for analyzing system requirements becomes increasingly important. Recent several studies have demonstrated that the cost of detecting and removing software errors increases significantly as the development process moves from requirements specification toward implementation and system integration. It has been estimated that the cost of removing an error from a system specification is an order of magnitude smaller than the cost of removing it from a system during integration testing. Modechart Toolset, developed at NRL and University of Texas (Austin), is an integrated prototype development environment for applying formal methods to the design and construction of real-time systems. This toolset supports the formal specification of real-time behavior in a language called Modechart and formal analysis via verification, simulation, and static consistency checks.
We are currently developing a monitoring and assertion checking tool to be integrated into the Modechart Toolset. Within this framework, we have developed a formal model for the problem of monitoring and assertion-checking based on computation prefixes. A major research issue is that not all assertions can be effectively monitored with a bounded event history. We have identified several powerful classes of assertions that can be evaluated by maintaining a bounded event history. In addition, we defined the necessary conditions for monitoring very general assertions by taking advantage of monotonicity properties of our specification language. Moreover, in a refinement of this approach, the semantics of Modechart have exploited to develop a class of assertions for which monitoring is simplified to evaluation of a state predicate. Ongoing work includes improving the testing capabilities of Modechart by increasing programmer control over the generation of execution traces, incorporating the effects of scheduling policies into the execution traces, and integrating specifications simulation and assertion-checking with formal verification techniques.