Insup Lee
Department of Computer and Information Science - University of Pennsylvania
Philadelphia PA 19104-6389, USA
FAX: 215 573-7362/573-8190
lee@cis.upenn.edu
http://www.cis.upenn.edu/~lee
Abstract
We describe the Monitoring-aided Checking and Steering (MaCS) framework that assures the correctness of the current execution at run-time. Checking is performed based on a formal specification of system requirements. Steering is to alter the system's behavior in response to violation of requirements. Our framework is to bridge the gap between formal verification and testing. The former is used to ensure the correctness of a design specification rather than an implementation, whereas the latter is to used to validate an implementation. An important aspect of the framework is clear separation between implementation-dependent description of monitored objects and high-level requirements specification. Another salient feature is automatic instrumentation of executable code for monitoring and steering.
The paper presents an overview of the framework and the three languages, which are used to specify what to observe from the running program, the requirements that the program must satisfy, and how to steer the running program to a safe state. This talk also briefly describes our current prototype implementation in Java as well as future work.
* Joint work with Sampath Kannan, Moonjoo Kim, Oleg Sokolsky, and Mahesh Viswanathan.
Last Updated: May 16, 2000 by Elisabetta Ferrando