SC207 Software Engineering
Term Paper 2002:

My Best View of A Topic in Software Engineering

Kuo Yien Kee

Nanyang Technological University
[email protected]
 

Software Topic:
Bandera : Extracting Finite-state Models from Java Source Code
Corbett, J.C.; Dwyer, M.B.; Hatcliff, J.; Laubach, S.; Pasareanu, C.S.; Robby; Hongjun Zheng
Page(s): 439 –448 Proceedings of the 22nd International Conference on Software Engineering, 2000. ICSE 2000

1 Introduction
In this paper, a software, Bandera is being introduced. The article discusses how the tool assists the analyst in the finite-state extraction from the Java source code to verify desired properties. A methodology on how the derivation of simplified and customized models from Java source code is also included. Finally, an illustration verifying a program using Bandera is presented.

2 Abstracts
The verification on desired property of an application is great facilitated by Bandera. Previously, Finite state verification techniques on software are unformulated, time consuming and error prone. With Bandera, existing sophisticated  techniques are now integrated with new ideas and concepts, thus showing promise as a cost-effective means for finding defects in software designs. The paper described how data abstraction can be done in the intermediate process of extracting finite states.

3 Contribution to the field of software engineering
Finite-state verification techniques, such as model checking, have shown promise as a cost-effective means for finding defects in hardware designs. To date, the application of these techniques to software has been hindered by several obstacle. Chief among these is the problem of constructing a finite-state model that approximates the executable behavior of the software system of interest. Current best practice involves hand-construction of models which is expensive (prohibitive for all but the smallest system), prone too error (which can result in misleading verification results), and difficult to optimize (which is necessary to combat the exponential complexity of verification algorithms).

With the introduction of Bandera, the finite-state building, optimizing and verification processes are simpler and  efficient and safe. After the Java source code and desired property prepositions are imported, Optimized finite state model can be built and exhaustive verification can be done and show counter-example and map it to the original source code if any defect is found, thus greatly reduced the load of human analyst to verify the program.

The Bandera is also capable of performing model checking on different existing templates such as SPIN and SMV. The Bandera also provide translator of the finite state model in the BIR format to tackle the semantic gap between the original source code and the input language of each supported model checker.

4 Elaboration of Techniques

Before we go into the details of major components of Bandera, we shall see the physiology of a model-checking software system.

Model checking is a technique for systematically searching the possible behaviors of a system for certain kinds of errors. First, the system (in our case, a Java program) is modeled as a finite­state transition system. Each state represents an abstraction of the program's state and each transition represents the execution of one or more statements transforming this state. Second, a desired property of the system is expressed in temporal logic [20]; the property describes some constraint on the permissible state/event sequences in the finite­state model. Third, a model checking tool algorithmically determines whether all paths through the finite­state transition system satisfy the property. If not, the model checker displays a path through the transition system violating the property; this path can be interpreted as a behavior of the system and used to understand the error.

The key to applying model checking to large software systems is not clever model checkers but clever model builders that abstract away most of the details of these programs, leaving only what is essential to verify a specific property. There are three main techniques that can be applied to build tractable models for verifying a given property: irrelevant component elimination, data abstraction, and component restriction.

I. Irrelevant component elimination : Many of the program components (classes, threads, variables, code) may not be relevant to the property being verified.

II. Data abstraction : After eliminating irrelevant components, some of the remaining variables, although relevant, might be recording more detail than is necessary for the property being verified. The range of such variables can often be safely abstracted to a much smaller set.

III. Component restriction : The two techniques above can often produce tractable models of software systems. If these methods fail, a restricted model of the program can usually be constructed by limiting the number of components and/or the ranges of variables. Note that the semantic gap between systems and finite state models is much wider for software than for hardware, and this may increase the need for component restriction.

Bandera consists of 4 major components:

• Slicer : The Bandera slicing component compresses paths in the program by removing control points, variables, and data structures irrelevant for checking a given property.

• Abstraction Engine : The Bandera abstraction engine allows the user to reduce the cardinality of data sets associated with variables. The tool also includes a language for specifying abstractions, which can be collected in an abstraction library for reuse.

• Back End : The back end of Bandera generates BIR: a low-level intermediate language based on guarded commands that abstracts common model check. The back end also contains a translator for each model checker supported 

• User Interface :  Bandera has an advanced graphical user interface that facilitates interaction with the various components and display counterexamples to the user in terms of the program source, like a debugger.

4.1 Soot/Jimple

As Bandera is built on top of the Soot compiler frame-work, thus in the beginning of the process, the Java Source code is translated to the intermediate language Jimple, which is supported by Soot. This is done with the front-end of Bandera called JJJC (Java-to Jimple-to-Java Compiler).

As the name suggested, the operation is bi-directional. JJJC has not only powerful translating function but also nodes, paths and return points capturing, tracing and mapping features. JJJC is also capable of provide appropiate presentation of Jimple-to-Java mapping even after transformations such as Slicing and Abstraction.

4.1 Slicer

Given a program P and some statements of interest C = {s₁, ..., s_k) from P called the slicing criterion, a program slicer will compute a reduced version of P.

This is done by extracting variables those related to the specification and exhaustedly check all the function and operations that will affect the value of those variables. As long as statement of P do not affect the satisfaction of the specification,  it will be removed.

The effectiveness of slicing of reducing program modules varies depending on the structure of the program. In some loosely coupled systems, slicing removes entire threads and dramatically reduces the state space, while in some other cases, where program components are tightly coupled or where large sections of the program are relevant to the specification, the slicing reduction is only moderate.

4.2 Abstraction-Based Specializer

Even after slicing, the variables remained might contain more data than we interest in, and in some other cases, when a specification to be checked does not depend on the program concrete values but instead depends on the properties of the values. For example, an integer variable x, according to its concrete value, can be assigned to different abstraction properties such as even-odd, positive-negative and true-false.

However, some information will be lost after abstraction and the operations that rely on those information can not be determined. Values that cannot be determined are represented with a special token T. When those tokens are passed to a conditional test, the choice is non-deterministic.

4.3 Back End

The Bandera back end is like a code generator. After the finite-state models of the program P is extracted, the data will flow into BIRC (Bandera Intermediate Representation Constructor) to generate a low level intermediate language called BIR (Bandera Intermediate Representation) which can be accepted by translators to produced the input languages of respective supported model checker.

4.4 Supplement Analyses

To improve the effectiveness of each components, aid of additional static analysis results are included in Bandera. Bandera is designed to allow the integration of a variety of analyses whose results can be used to boost the precision of the primary model extraction transformations so as to produce more accurate and compact models.

4.5 User Interface

Bandera toolsets provides both a command line and a graphical user interface, called the Bandera User Interface (BUR). The BUR includes source level code view, with highlights of sliced locations, abstracted variables and return points locations, check property configuration and counterexample stepping navigator.

5 Related Articled Published
_{Slicing Software for Model Construction (1999)
John Hatcliff, Matthew B. Dwyer, Hongjun Zheng Higher-Order and Symbolic Computation}

Slicing Multi-threaded Java Programs: A Case Study (1999)
Matthew B. Dwyer, James C. Corbett, John Hatcliff, Stefan Sokolowski, Hongjun Zheng Partial Evaluation and Semantic-Based Program Manipulation

_{Using the Bandera Tool Set to Model-check Properties of Concurrent Java Software 
John Hatcliff and Matthew Dwyer SAnToS Laboratory, Department of Computing... International Conference on Concurrency Theory}

6 Relation to My Lab Project
The reveal of  methodology of slicing, abstraction and component restriction have given me an idea about testing and searching the defects by finite-state modeling. Unfortunately, this paper doesn't seem have any direct relation to my Lab Project, as the program is not written in Java.. The knowledge obtained from this paper is not enough to be perform such testing on my lab project manually.

 

7 Possible Extensions
_{The current Bandera is still not capable to handle some of  the features of a Java program including dynamic allocation handling, garbage collection and etc. It is promised these limitation will be lifted in the next version when  additional tool capabilities are integrated. There is a possibility that Bandera will be developed as an optimized Java compiler with debugger and model checking utilities. Similar toolset can be developed for C and C++ programs.}

8 Comments on the Notification/Diagram
_{There isn't any significant notification and diagram except basic preposition notations revealed in this paper. Therefore no appropriate comment about this should be made by myself.}

9 Comments
_{• Software Project
The Bandera discussed in the article is an efficient tool that analyst, programmer and tester should try to use in their software development process. I personally feel that it may also be possible to introduce this tool to software engineering students to help them analyze defects their JAVA program, especially in SC204, Concurrency course.}

<sub>• Process
At the moment, the Bandera is not yet fully developed, and there is much space of expansion can be foreseen.

• Platform
Bandera should be able to work on Window-based platform.</sub>

<sub>• People
James C. Corbett,  the main author of the article, is Associate Professor Department of
Information and Computer Science at University of Hawai'i.

• Product
Bandera is an integrations of existing toolsets with advanced algorithms and yet flexibly reserves spaces for toolsets which will be developed in the future.</sub>
 

10 Comments on the Results

The table shown above is the data obtained after using Bandera on a Java program. The data obviously shows the benefits of property directed slicing and abstraction in model extraction. The notation b stands for original source code, d stands for modified source code with defective conditions , while r and p are two different property we interest in, with index represent different stages or objects. n stands for no transformation made on the source code, s stands for slicing and a stands for both slicing and abstraction.

From experiments we found that slicing is easy and effective to reduce the finite-state. In the other hand, best abstraction, i.e., ones that give maximal reduction but preserve the property being checked, is a difficult problem. However, initial experience suggests that even naive abstraction choices are often effective. 

11 References

1. J. C. Corbett. Evaluating deadlock detection methods for concurrent software.
IEEE Transaction on Software Engineering
22(3), Mar.1996.

2. J. C. Corbett. Constructing Compact models of concurrent Java programs. 
Proceedings of the 1998 International Symposium on Software Testing and Analysis (ISSTA),
ACM Press, March 1998 

3. SC207 Software Engineering Lecture Notes
Nanyang Technological University

Click here for Word Document format of this report