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 article

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 1 2001
EventRV'2001, Runtime Verification (in Connection with CAV '01) - Paris, France
Duration: Jul 23 2001Jul 23 2001

Fingerprint

Java
Monitoring
Formal methods
Formal Specification
Formal Methods
Prototype
Requirements Specification
Formal Verification
Instrumentation
Correctness
Complement
Specifications
Testing
Target
Architecture
Dependent
Requirements

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Java-MaC : A run-time assurance tool for Java programs. / Kim, M.; Kannan, S.; Lee, I.; Sokolsky, O.; Viswanathan, M.

In: Electronic Notes in Theoretical Computer Science, Vol. 55, No. 2, 01.10.2001, p. 218-235.

Research output: Contribution to journalConference article

Kim, M. ; Kannan, S. ; Lee, I. ; Sokolsky, O. ; Viswanathan, M. / Java-MaC : A run-time assurance tool for Java programs. In: Electronic Notes in Theoretical Computer Science. 2001 ; Vol. 55, No. 2. pp. 218-235.
@article{2e0f75dde704444a8207ebdce4817b2f,
title = "Java-MaC: A run-time assurance tool for Java programs",
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.",
author = "M. Kim and S. Kannan and I. Lee and O. Sokolsky and M. Viswanathan",
year = "2001",
month = "10",
day = "1",
doi = "10.1016/S1571-0661(04)00254-3",
language = "English (US)",
volume = "55",
pages = "218--235",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "2",

}

TY - JOUR

T1 - Java-MaC

T2 - A run-time assurance tool for Java programs

AU - Kim, M.

AU - Kannan, S.

AU - Lee, I.

AU - Sokolsky, O.

AU - Viswanathan, M.

PY - 2001/10/1

Y1 - 2001/10/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=19144373771&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=19144373771&partnerID=8YFLogxK

U2 - 10.1016/S1571-0661(04)00254-3

DO - 10.1016/S1571-0661(04)00254-3

M3 - Conference article

AN - SCOPUS:19144373771

VL - 55

SP - 218

EP - 235

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 2

ER -