Abstract
We describe Java-MaC, a prototype implementation of the Monitoring and Checking (MaC) architecture for Java programs. The MaC architecture provides assurance about the correct execution of target programs at run-time. Monitoring and checking is performed based on a formal specification of system requirements. MaC bridges the gap between formal verification, which ensures the correctness of a design rather than an implementation, and testing, which only partially validates an implementation. Java-MaC provides a lightweight formal method solution as a viable complement to the current heavyweight formal methods. An important aspect of the architecture is the clear separation between monitoring implementation-dependent low-level behaviors and checking high-level behaviors against a formal requirements specification. Another salient feature is automatic instrumentation of executable codes. The paper presents an overview of the MaC architecture and a prototype implementation Java-MaC.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 218-235 |
| Number of pages | 18 |
| Journal | Electronic Notes in Theoretical Computer Science |
| Volume | 55 |
| Issue number | 2 |
| DOIs | |
| State | Published - Oct 2001 |
| Externally published | Yes |
| Event | RV'2001, Runtime Verification (in Connection with CAV '01) - Paris, France Duration: Jul 23 2001 → Jul 23 2001 |
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)