Java-MaC: A Run-Time Assurance Approach for Java Programs

Moonzoo Kim, Mahesh Viswanathan, Sampath Kannan, Insup Lee, Oleg Sokolsky

Research output: Contribution to journalArticlepeer-review

Abstract

We describe Java-MaC, a prototype implementation of the Monitoring and Checking (MaC) architecture for Java programs. The MaC architecture provides assurance that the target program is running correctly with respect to a formal requirements specification by monitoring and checking the execution of the target program at run-time. MaC bridges the gap between formal verification, which ensures the correctness of a design rather than an implementation, and testing, which does not provide formal guarantees about the correctness of the system. Use of formal requirement specifications in run-time monitoring and checking is the salient aspect of the MaC architecture. MaC is a lightweight formal method solution which works as a viable complement to the current heavyweight formal methods. In addition, analysis processes of the architecture including instrumentation of the target program, monitoring, and checking are performed fully automatically without human direction, which increases the accuracy of the analysis. Another important feature of the architecture is the clear separation between monitoring implementation-dependent low-level behaviors and checking high-level behaviors, which allows the reuse of a high-level requirement specification even when the target program implementation changes. Furthermore, this separation makes the architecture modular and allows the flexibility of incorporating third party tools into the architecture. The paper presents an overview of the MaC architecture and a prototype implementation Java-MaC.

Original languageEnglish (US)
Pages (from-to)129-155
Number of pages27
JournalFormal Methods in System Design
Volume24
Issue number2
DOIs
StatePublished - Mar 2004

Keywords

  • Execution trace validation
  • Formal specification
  • Java
  • Java bytecode engineering
  • Program instrumentation
  • Run-time monitoring and checking
  • Software reliability

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Java-MaC: A Run-Time Assurance Approach for Java Programs'. Together they form a unique fingerprint.

Cite this