IBOC: The IMCOS Boundedness Checker
IBOC is a buffer boundedness checker for Rational Rose RealTime models or Promela models. Given a model, it checks if all communication buffers in the model contain only a bounded number of messages at run time. In case that IBOC determines the model to be bounded, it also delivers an estimated bound for each individual buffer. IBOC is written in Visual C++ and equipped with a graphic user interface. It uses "lp_solve" as its ILP solving engine, and uses the runtime environment of the IBM Rational Rose RealTime tool (now a part of Rational Rose Technical Developer) to retrieve information of a Rose RealTime model. Currently, it runs only on Windows.
The Theory Behind
The theoretical foundation of buffer boundedness checking is based on the papers [LMW04a], [LMW04b], and [LW05]. The basic idea is described as the following.
Given a model, a certain set of details of the model are first abstracted away, among which are all program code except the message sending and receiving statements, message orders, and dependencies of the executions of control flow cycles in the model. As a result, we obtain a set of control flow cycles. Each of these cycles has an integer vector, called effect vector, in which each component corresponds to one type of messages and denotes how many messages of this type are sent (by a positive number) or consumed (by a negative number) by the cycle. On the effect vectors of the collected cycles, we can give a necessary condition for the existence of an unbounded buffer. Intuitively, this condition describes a situation in which there is a way to combine the executions of a certain set of cycles such that the combined effect does not consume any messages and sends at least one message of some type. Such a combination can be repeated without constraints to flood some buffers. If the situation described above does not exist, then all buffers remain bounded at run time. This necessary condition is encoded into an Integer Linear Programming (ILP) problem. If there is no solution to this ILP problem, then we are assured of the boundedness of the model. Otherwise, no conclusion can be drawn, and in this case we shall enter the refinement procedure.
Remember that we do abstractions in our boundedness checking method. Abstractions can make the analysis more efficient, but they also introduce imprecision -- they may include behavior that the original model does not exhibit. So, when the boundedness checking ILP problem has solutions, we do not know if the model is bounded or not. When this is the case, a counterexample is constructed from a particular solution to the ILP problem. Note that each solution to the ILP problem corresponds to a certain combination of cycle executions. The counterexample constructed from an ILP solution is then the set of all cycles that are executed in the corresponding combination. This counterexample may be not real because of the presence of the spurious behavior introduced by the abstractions. In order to exclude unreal cycle combinations, we use some static analysis techniques to discover dependencies among cycles. The underlying idea is to find out, in order to let a cycle to be executed infinitely often, which other cycles may have to be executed also infinitely often. This is achieved by examining the executability of cycles. The estimated cycle dependencies can be encoded into linear inequalities to augment the original ILP problem, thereby refining the abstraction. The refined abstraction is then subject to the next iteration of boundedness checking.
As seen above, the whole boundedness checking is an iterative procedure. The abstraction of a model is gradually refined as driven by the counterexamples constructed during the checking. The checking procedure terminates with either a "BOUNDED" verdict, or an "UNKNOWN" verdict when it fails to further refine the abstraction. This means our method is incomplete. But it is anyhow inevitable because the buffer boundedness problem is undecidable for any Rose RealTime or Promela models.
Usage & Screenshots
Here we show the usage of IBOC with a screenshot.
The checking of Rose RealTime models and Promela models both require some manual pre-processing work. For a Rose RealTime model, the arbitrary program code on the transitions in the model must be manually abstracted into sequences of message sending statements, for the lack of the automated code abstraction support for Rose RealTime models. For a Promela model, one has to use the following SPIN commands to generate two files from the model: a "*.cfsm" file containing a textual reprensentation of the state machine behavior of each proctype; and a "*.sym" file containing the list of identifiers/symbols used in the model.
spin -a MODEL_FILE gcc -c pan pan.c pan -d > MODEL_FILE.cfsm spin -d > MODEL_FILE.sym
The left shows the main user interface of IBOC. Here a user can choose a model to be checked. After a model is chosen, the "check" button will be enabled. A click on this button will start the checking procedure. IBOC also allows a user to select some of the components in a model for the boundedness checking. This enables the user to check if a certain part of the model is bounded. This is helpful to find the source of unboundedness. For Rose RealTime models, you are granted an option to accept "non-trigger transitions", which are spontaneous transitions that need no incoming messages to trigger their firings. With this option we can check a partly completed model in the middle of software design procedures.
The result of a boundedness test is displayed in the main text box on the "Running Output" tab. The output includes the list of collected cycles and their effect vectors, estimated buffer bounds, discovered cycle dependencies, etc. The generated ILP problem can also be viewed when the "LP Problem" tab is shown. Both the output and the ILP problem can be saved for future inspections.
There are two implementations of IBOC. The first implementation, as shown in the above screenshot, was started in 2003 around the time when the research on buffer boundedness was initialized. The further development and maintenance of this implementation have been discontinued since September 2005. Therefore, it does not feature the latest improvement on cycle dependency discovery techniques used in the abstraction refinement procedure.
The second implementation of IBOC resulted from a modification of the source code of another property checking tool "aLive" that we developed. It can be deemed as an improved version of the previous IBOC. However, this version checks only Promela models, and the buffer bound estimation procedure is still missing. Also, it does not have a GUI.
Both implementations of IBOC are not ready for public release. A future public release of IBOC is within our plan. At the moment, if you are interested to obtain an immature version, please feel free to contact us.
Aside from bug fixing, we have the following plans for the future development.
- We will enhance the user interface of IBOC, eliminating as much as possible the need of manual processing.
- We will integrate more advanced techniques into IBOC to improve both the efficiency and the precision of the boundedness test.
- We aim to build an open software model verification tool set based on the ILP solving techniques that we develop within the IMCOS project. This would bring better code reuseability and extendability for the implementation of other property checking methods. We will first integrate the buffer boundedness test and the livelock freedom test into the tool set.