This paper investigates implementations of process algebras which are suitable for modeling concurrent real-time systems. It suggests an approach for efficiently implementating real-time semantics using dynamic priorities. For this purpose a process algebra with dynamic priority is defined whose semantics corresponds one-to-one to traditional real-time semantics. The advantage of the dynamic-priority approach is that it drastically reduces the state-space sizes of the systems in question while preserving all properties of their functional and real-time behavior.
The utility of the technique is demonstrated by a case study which deals with the formal modeling and verification of several aspects of the widely-used SCSI-2 bus-protocol. The case study is carried out in the Concurrency Workbench of North Carolina, an automated verification tool in which the process algebra iwth dynamic priority is implemented. It turns out that the state space of the bus-protoocol is about an order of magnitude smaller than the one resulting from real-time semantics. The accuracy of the model is proved by applying model checking for verifying several mandatory properties of the bus-protocol.
Process algebra represents a mathematically rigorous framework for modeling concurrent systems of interacting processes. The process-algebraic approach relies on equational and inequational reasoning as the basis for analyzing the behavior of such systems. This chapter surveys some of the key results obtained in the area within the setting of a particular process-algebraic notation, the Calculus of Communicating Systems (CCS) of Milner. In particular, the Structural Operational Semantics approach to defining operational behavior of languages is illustrated via CCS, and several operational equivalences and refinement orderings are discussed. Mechanisms are presented for deducing that systems are related by the equivalence relations and refinement orderings, and different process-algebraic modeling formalisms are briefly surveyed.
This paper presents a mu-calculus-based modal logic for describing properties of probabilistic labeled transition systems (PLTSs) and develops a model-checking algorithm for determining whether or not states in finite-state PLTSs satisfy formulas in the logic. The logic is based on the distinction between (probabilistic) "systems" and (nonprobabilistic) "observations": using the modal mu-calculus, one may specify sets of observations, and the semantics of our logic then enables statements to be made about the measures of such sets at various system states. The logic may be used to encode a variety of probabilistic modal and temporal logics; in addition, the model-checking problem for it may be reduced to the calculation of solutions to systems of non-linear equations.
A common problem in library-based programming is the downward compatibility problem: will a program using an existing version of a library continue to function correctly with an upgraded version? As a step toward addressing this problem for libraries of reactive components we develop a theory that equips components with interface languages characterizing the interaction patterns user applications may engage in with the component. We then show how these languages may be used to build upgrade specifications from components and their interface languages. Intuitively, upgrade specifications explicitly describe requirements an (improved) implementation of a component must satisfy and are intended for use by library developers. Under certain reasonable assumptions about the contexts components are to be used in we show that our upgrade specifications are complete in the sense that every correct upgrade of a component is related in a precise manner to its upgrade specification. In particular, these results hold if the language being used to develop contexts is CSP or CCS.
Our model-checking results show that (for a particular network configuration) RETHER makes good on its bandwidth guarantees to real-time nodes without exposing non-real-time nodes to the possibility of starvation. Our data also indicate that, in many cases, the state-exploration overhead of the local model checker is significantly smaller than the total amount that would result from a global analysis of the protocol.
In the course of specifying and verifying RETHER, we also identified an alternative design of the protocol that warranted further study due to its potentially smaller run-time overhead in servicing requests for data transmission. Again, using local model checking, we showed that this alternative design also possesses the properties of interest. This observation points up one of the often-overlooked benefits of formal verification: by forcing designers to understand their designs rigorously and abstractly, these techniques often enable the designers to uncover interesting design alternatives.
Finally, we give proof techniques, derived from the alternative characterizations, for establishing preorder relationships between probabilistic processes. The utility of these techniques is demonstrated by means of some simple examples.
| Go to Rance Cleaveland's publication home page. |