About RAPA

Short version: Verification techniques analyze software (or hardware) for bugs: behaviors that are unwanted, often unexpected, and can cause an application to end up in an unworkable state, crash, or simply compute wrong results. This project develops a verification technique that exploits the fact that most software systems are designed over a variable number of resource instances. How do changes (especially incremental changes) of the instance parameter affect the behavior of the software?

More details: Many systems are naturally designed (consciously or not) over a variable number of certain resources, which can mean physical or logical entities. Examples of such resources include:

• the number of physical components of a certain functional type,
• the number of clients that simultaneously request a service from a server,
• the capacity of the communication channel between components,
• the number of context switches permitted among concurrent threads,
• the recursion nesting depth (= stack size) permitted in a piece of software.

We can expect that the behavior of the instances of the parametric design family (= the concrete designs for each parameter choice) depend on the parameter in a smooth, "continuous" way. This enables analyses of the function that maps the number of resource instances (= the parameter) to a concrete design (this function goes from the natural numbers to the design space).

More concretely, suppose k is an integral parameter of the design. With the target property P to be verified in mind, we define a function O mapping the parameter to observations about the design of size k, such that knowledge of O(k) enables a decision on whether P holds of the instance of size k. For example, the "observation" could simply be the set of states reachable in the system of size k.

In general, we require of function O that it be monotone: more resources means more system behaviors (observations). This is almost always the case provided the value of k is not accessible in the program defining a system instance's behavior. (If it is, the dependence on k can be arbitrary, making analysis against unbounded k in general impossible.)

We now analyze the system design for increasing values of k. Due to monotonicity of O, consecutive observation sets O(k) are in some sort of ≤ relationship. This begs the question whether the function O converges at some parameter point k0, i.e. whether it stops increasing after reaching k0. If so, the truth value of property P has stabilized, i.e. unless we have detected a violation of P up to this point, we have proved the property for all parameter instances.

Research Sponsors: