Beyond Correctness

  For sequential programs, correctness is the paramount requirement and can be modeled as a function relating inputs to outputs. A correct sequential program should also terminate for all inputs.

For concurrent systems, particularly those of the reactive variety, many other requirements, of a non-functional nature, play a role. These include the following:

timeliness

Many concurrent systems are subjected to timing constraints, e.g., if the amount of water in a water pump exceeds a certain level then the pump should shut off within t seconds. Embedded systems, which interact with their environment through sensors and actuators, are a typical example of a class of concurrent systems for which real-time behavior is a major concern, and performance requirements must be met.

fault tolerance

Concurrent systems must often provide continuous service (i.e., be reliable) despite the occurrence of various types of failures. This is especially important for safety-critical systems.

availability

If a system (component) crashes, the down-time must be kept to a minimum by appropriate constructive measures.

security

As systems become more distributed and more accessible, it is increasingly important to make them resistant against passive or active misuse by intruders.

safety

Besides being correct under a given fault hypothesis, concurrent systems must obey a well-defined failure behavior like fail-stop of fail-soft (graceful degradation).

mobility

In a mobile computing system, the configuration of communication links between agents and the code executed by agents changes dynamically. Such mobility is achieved through a liberal interpretation as to what constitutes a message; i.e., links and code can be sent from one agent to another.

Note that these different types of requirements are sometimes contradictory. Reliability, for instance, requires the use of additional resources, which may degrade system performance and thus endanger timeliness.

Although traditional research on program correctness has focused on sequential programs, recent work has produced a number of specification and verification techniques that address issues peculiar to concurrent systems. For example, substantial progress has been made on models and logics for

real-time, probability (useful e.g. for specifying and analyzing system faults), and mobility.

Regarding future work in this area, we should solidify our understanding of phenomena such as real-time and mobility (e.g., there is an ongoing debate over the use of dense-time vs. discrete-time in real-time models), and at the same time develop new formalisms for those phenomena that remain largely unexplored (e.g., security). Achieving these goals will likely necessitate interaction with researchers from other computer science disciplines, and from non-computer-science disciplines such as electrical and mechanical engineering and control theory.

We should also strive to develop semantical partnerships between formalisms that would facilitate the construction of a model that captures the subset of requirements most relevant to a given problem; e.g., a model that embodies timing and probability information in the context of mobile systems.

Finally, it behooves us to bring these formalisms out of the ``test-tube'' environment and apply them in an integrated way to the specification, verification and design of complex real-life systems. A concrete challenge here is the formal modeling and analysis of the emerging micro electro-mechanical systems (MEMS) technology. A MEMS system represents a host of computational and mechanical modeling challenges on a single piece of silicon.