Electronic Notes in Theoretical Computer Science 55 No. 2 (2001)
URL: http://www.elsevier.nl/locate/entcs/volume55.html 18 pages
Java-MaC: a Run-time Assurance Tool for Java
Programs
M. Kim, S. Kannan, I. Lee, O. Sokolsky 1
Department of Computer and Information Science
University of Pennsylvania
Philadelphia, US
M. Viswanathan 2
DIMACS & Telcordia Technologies
Piscataway, US
Abstract
We describe Java-MaC, a prototype implementation of the Monitoring and Check-
ing (MaC) architecture for Java programs. The MaC architecture provides assur-
ance about the correct execution of target programs at run-time. Monitoring and
checking is performed based on a formal speci cation of system requirements. MaC
bridges the gap between formal veri cation, which ensures the correctness of a design
rather than an implementation, and testing, which only partially validates an im-
plementation. 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
speci cation. Another salient feature is automatic instrumentation of executable
codes. The paper presents an overview of the MaC architecture and a prototype
implementation Java-MaC.
1 Introduction
In the past two decades, much research has concentrated on the methods
for analysis and validation of software systems as such systems have been
deployed in safety critical areas including avionics and automobiles. Many
successful industrial case studies have been conducted in the area of formal
veri cation [4]. Complete formal veri cation, however, has not yet become
1 Email: fmoonjoo,kannan,lee,
2 Email:
c 2001 Published by Elsevier Science B. V.
, Kim et al
a prevalent analysis method. Reasons for this are twofold. First, complete
veri cation of real-life systems remains infeasible. The growth of software size
and complexity seems to exceed advances in veri cation technology. Second,
veri cation results apply not to system implementations, but to formal models
of these systems. That is, even if a design has been formally veri ed, it still
does not ensure the correctness of a particular implementation of the design.
This is because an implementation often is much more detailed, and also may
not strictly follow the formal design. So, there are possibilities for introduction
of errors into an implementation of the design that has been veri ed. One way
that people have traditionally tried to overcome this gap between design and
implementation has been to test an implementation on a pre-determined set
of input sequences. This approach, however, fails to provide guarantees about
the correctness of the implementation on all possible input sequences.
Consequently, when a system is running, it is hard to guarantee whether
or not the current execution of the system is correct using the two traditional
methods. Therefore, the approach of continuously monitoring a running sys-
tem with respect to a formal requirement speci cation can be used to ll the
gap between these two approaches. This approach might not seem very useful
at rst glance because detecting errors does not seem interesting; just report-
ing a system crash is not helpful. However, run-time monitoring helps users
detect and correct errors. First, subtle errors are hard to detect without thor-
ough run-time monitoring and checking [16]. Second, errors may not cause
disastrous system failure immediately. Run-time monitoring and checking can
nd such errors quickly and help users take a recovery action before critical
failure happens.
In this paper, we describe the Monitoring and Checking (MaC) architec-
ture whose aim is to provide assurance that the target program is running
correctly with respect to a formal requirement speci cation. Use of formal
requirement speci cations in run-time monitoring is the salient aspect of the
MaC architecture. The MaC architecture is a general architecture not lim-
ited to any speci c programming language. To demonstrate the e ectiveness
of the MaC architecture, however, we have implemented a MaC prototype
for Java programs called Java-MaC. Java-MaC instruments Java executable
codes (bytecodes) automatically. This automatic instrumentation, along with
automatic generation of the run-time components of Java-MaC, enables easy
deployment of Java-MaC.
The paper is organized as follows. Section 2 presents an overview of the
MaC architecture. Section 3 brie y presents the languages for requirement
speci cations. Section 4 discusses issues on how to extract information from
the execution of a Java program. Section 5 describes the Java-MaC imple-
mentation. Section 6 illustrates a stock client example. Section 7 presents
related work. Finally, section 8 summarizes and concludes the paper. More
complete treatment of Java-MaC is given in [10].
2
, Kim et al
2 Overview of the MaC Architecture
The overall structure of the architecture is shown in Fig 1. The architecture
includes two main phases: static phase and run-time phase. From a target
program and a formal requirement speci cation, the static phase (before a
target program runs) automatically generates run-time components including
a lter, an event recognizer, and a run-time checker. In the run-time phase
(during the execution of a target program), information of the target program
execution is collected and checked against given formal requirement speci ca-
tion.
Fig. 1. Overview of the MaC architecture
2.1 Static phase
A major task during the static phase is to provide a mapping between high-
level events used in the high-level requirement speci cation and low-level state
information extracted from the instrumented target program during execu-
tion. These are related explicitly by means of a low-level speci cation. The
low-level speci cation describes how events at the high-level requirement are
de ned in terms of monitored states of a target program. For example, in
a gate controller of a railroad crossing system, the requirements may be ex-
pressed in terms of the event train in crossing. The target program, on the
other hand, stores train's position with respect to the crossing in a variable
train position. The low-level speci cation in this case can de ne the event
train in crossing as train position < 800.
Another major task during the static phase is to generate run-time compo-
nents. A lter is generated from the low-level speci cation and inserted into
the target program automatically. An event recognizer is generated from the
low-level speci cation automatically. Similarly, a run-time checker is gener-
ated automatically from the high-level speci cation.
3
URL: http://www.elsevier.nl/locate/entcs/volume55.html 18 pages
Java-MaC: a Run-time Assurance Tool for Java
Programs
M. Kim, S. Kannan, I. Lee, O. Sokolsky 1
Department of Computer and Information Science
University of Pennsylvania
Philadelphia, US
M. Viswanathan 2
DIMACS & Telcordia Technologies
Piscataway, US
Abstract
We describe Java-MaC, a prototype implementation of the Monitoring and Check-
ing (MaC) architecture for Java programs. The MaC architecture provides assur-
ance about the correct execution of target programs at run-time. Monitoring and
checking is performed based on a formal speci cation of system requirements. MaC
bridges the gap between formal veri cation, which ensures the correctness of a design
rather than an implementation, and testing, which only partially validates an im-
plementation. 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
speci cation. Another salient feature is automatic instrumentation of executable
codes. The paper presents an overview of the MaC architecture and a prototype
implementation Java-MaC.
1 Introduction
In the past two decades, much research has concentrated on the methods
for analysis and validation of software systems as such systems have been
deployed in safety critical areas including avionics and automobiles. Many
successful industrial case studies have been conducted in the area of formal
veri cation [4]. Complete formal veri cation, however, has not yet become
1 Email: fmoonjoo,kannan,lee,
2 Email:
c 2001 Published by Elsevier Science B. V.
, Kim et al
a prevalent analysis method. Reasons for this are twofold. First, complete
veri cation of real-life systems remains infeasible. The growth of software size
and complexity seems to exceed advances in veri cation technology. Second,
veri cation results apply not to system implementations, but to formal models
of these systems. That is, even if a design has been formally veri ed, it still
does not ensure the correctness of a particular implementation of the design.
This is because an implementation often is much more detailed, and also may
not strictly follow the formal design. So, there are possibilities for introduction
of errors into an implementation of the design that has been veri ed. One way
that people have traditionally tried to overcome this gap between design and
implementation has been to test an implementation on a pre-determined set
of input sequences. This approach, however, fails to provide guarantees about
the correctness of the implementation on all possible input sequences.
Consequently, when a system is running, it is hard to guarantee whether
or not the current execution of the system is correct using the two traditional
methods. Therefore, the approach of continuously monitoring a running sys-
tem with respect to a formal requirement speci cation can be used to ll the
gap between these two approaches. This approach might not seem very useful
at rst glance because detecting errors does not seem interesting; just report-
ing a system crash is not helpful. However, run-time monitoring helps users
detect and correct errors. First, subtle errors are hard to detect without thor-
ough run-time monitoring and checking [16]. Second, errors may not cause
disastrous system failure immediately. Run-time monitoring and checking can
nd such errors quickly and help users take a recovery action before critical
failure happens.
In this paper, we describe the Monitoring and Checking (MaC) architec-
ture whose aim is to provide assurance that the target program is running
correctly with respect to a formal requirement speci cation. Use of formal
requirement speci cations in run-time monitoring is the salient aspect of the
MaC architecture. The MaC architecture is a general architecture not lim-
ited to any speci c programming language. To demonstrate the e ectiveness
of the MaC architecture, however, we have implemented a MaC prototype
for Java programs called Java-MaC. Java-MaC instruments Java executable
codes (bytecodes) automatically. This automatic instrumentation, along with
automatic generation of the run-time components of Java-MaC, enables easy
deployment of Java-MaC.
The paper is organized as follows. Section 2 presents an overview of the
MaC architecture. Section 3 brie y presents the languages for requirement
speci cations. Section 4 discusses issues on how to extract information from
the execution of a Java program. Section 5 describes the Java-MaC imple-
mentation. Section 6 illustrates a stock client example. Section 7 presents
related work. Finally, section 8 summarizes and concludes the paper. More
complete treatment of Java-MaC is given in [10].
2
, Kim et al
2 Overview of the MaC Architecture
The overall structure of the architecture is shown in Fig 1. The architecture
includes two main phases: static phase and run-time phase. From a target
program and a formal requirement speci cation, the static phase (before a
target program runs) automatically generates run-time components including
a lter, an event recognizer, and a run-time checker. In the run-time phase
(during the execution of a target program), information of the target program
execution is collected and checked against given formal requirement speci ca-
tion.
Fig. 1. Overview of the MaC architecture
2.1 Static phase
A major task during the static phase is to provide a mapping between high-
level events used in the high-level requirement speci cation and low-level state
information extracted from the instrumented target program during execu-
tion. These are related explicitly by means of a low-level speci cation. The
low-level speci cation describes how events at the high-level requirement are
de ned in terms of monitored states of a target program. For example, in
a gate controller of a railroad crossing system, the requirements may be ex-
pressed in terms of the event train in crossing. The target program, on the
other hand, stores train's position with respect to the crossing in a variable
train position. The low-level speci cation in this case can de ne the event
train in crossing as train position < 800.
Another major task during the static phase is to generate run-time compo-
nents. A lter is generated from the low-level speci cation and inserted into
the target program automatically. An event recognizer is generated from the
low-level speci cation automatically. Similarly, a run-time checker is gener-
ated automatically from the high-level speci cation.
3
