Analyzing Open Programs

Question

Describe the term Analyzing Open Programs?

Answer 1

A key problem in software model checking is environment modeling. Software model checkers such as JPF or SPIN can analyze only closed, executable programs—that is, programs that operate on fully specified inputs. However, most software systems are fundamentally open, since their behavior is dependent on patterns of invocation of system components and values defined outside the system but referenced within the system. Whether you are reasoning about the behavior of whole programs or about program components, a model of the environment is therefore essential in enabling model checking.

An environment model for a software component (unit) establishes an abstract runtime context in which the unit executes. It contains both data information (e.g., values that flow into the unit) and control information (e.g., a sequence of method invocations in the unit interface) that influence the unit under analysis. This model should be small enough to enable tractable verification, but sufficiently detailed to not mask property violations.

Environment models allow developers to analyze individual units early in the software lifecycle, when they become code complete, and possibly before the whole software system has been developed and integrated. In this case, model checking is used as an adjunct to unit testing, and the environment models play the role of a testing harness. Environment models are also used in the context of verifying large systems: The system can be broken up into smaller parts which can be verified separately and more efficiently. In this case, the environment model for an analyzed component represents the rest of the system with which the component interacts. The environment encodes only the interface behavior and is much smaller than the actual components it represents, enabling more efficient verification. Environments can also be used to model non-source-code components (for example, hardware components when analyzing embedded software) and native libraries that cannot be analyzed directly by a software model checker.