Java-MaC: A run-time assurance tool for Java programs

M. Kim, S. Kannan, I. Lee, O. Sokolsky, M. Viswanathan

Research output: Contribution to journalConference articlepeer-review

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 languageEnglish (US)
Pages (from-to)218-235
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Volume55
Issue number2
DOIs
StatePublished - Oct 2001
Externally publishedYes
EventRV'2001, Runtime Verification (in Connection with CAV '01) - Paris, France
Duration: Jul 23 2001Jul 23 2001

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Java-MaC: A run-time assurance tool for Java programs'. Together they form a unique fingerprint.

Cite this