Model checking is a state-space exploration technique for automatically verifying digital systems against specifications stated in temporal logics. With the advent of Binary Decision Diagrams (BDDs) which allow for compact symbolic representations of state spaces, model checking became applicable to verifying real-world hardware systems and synchronous software systems. Symbolic model checking currently receives significant attention in industry, especially for validating hardware designs.
Unfortunately, asynchronous systems, such as event-driven distributed software systems, give rise to extremely large state spaces for which state-space generation and exploration are not only memory-bound problems, but also time-bound problems. Recent research has made significant progress for generating state spaces of such systems. The developed algorithms (i) employ Multi-valued Decision Diagrams (MDDs) for approaching the first problem and (ii) exploit the notion of event locality inherent in asynchronous systems for dealing with the second problem.
Further interest is in the systematic investigation of design decisions made for these algorithms and in employing the algorithms as a basis for symbolic model checking. The notion of event locality also provides new ideas for the algorithms' parallelization with respect to shared-memory and distributed-memory architectures, especially on networks of workstations and PC clusters. This is of particular importance as existing parallelizations of model checkers do not show any significant speed-ups. The high complexity of the algorithms to be developed also demands formal proofs of their correctness. Finally, their utility needs to be demonstrated by conducting case studies and performance studies.
This project is part of a collaboration with Prof. Gianfranco Ciardo at the College of William and Mary, Williamsburg, Virginia, USA.
Engineers frequently use a mixture of operational and declarative styles for specifying real-world systems. As an example one might want to consider the popular Unified Modelling Language (UML) used for software specification and design, which incorporates both state machines (including Statecharts and Message Sequence Charts) for specifying system behaviour and a declarative language for specifying constraints between objects (the Object Constraint Language OCL).
Unfortunately, design formalisms have traditionally employed either an operational style of specification, such as supported by process algebras, or a declarative style, such as advocated by the temporal logic school. The goal of the proposed research is to define new heterogeneous specification languages combining process algebras and temporal logics and to develop their algebraic theories based on refinement preorders which relate system specifications and (partial) system designs. The refinement preorders should be compatible with traditional process-algebraic refinement preorders and, in addition, the satisfaction relations of temporal logics. Intuitively, these preorders should be employed for ensuring the correctness when gradually transitioning from system specifications to system designs. Further, the new framework should be investigated algebraically and algorithmically by providing axiomatizations of and decision procedures for the refinement preorders.
In order to demonstrate the utility of the new theory for engineering practice, it is planned to front-end the new languages by visual design notations combining ideas of interfacing Statecharts to process algebras and of extensions of message sequence charts targeted towards expressing temporal properties. A prototypic tool will provide the framework for integrating the new languages and notations together with the developed decision procedures for the considered refinement preorders.
This project is part of a collaboration with Prof. Rance Cleaveland at the State University of New York at Stony Brook, USA.
Process Algebras are formalisms for modelling and reasoning about the communication behaviour of reactive systems. In the past decade, traditional process algebras, such as CCS, have been extended for capturing the dynamic aspect of mobility within systems. Examples for mobility include the name passing inherent in object-oriented languages and dynamic re-configurations of networks. A prominent process algebra for expressing mobility, which is derived from CCS, is the pi-calculus.
Many existing systems, however, not only involve mobility, but also priority and real-time. The latter aspects are semantically based the concept of pre-emption, which arises when a communication on one system channel should be given precedence over a communication on some other channel. While the concept of pre-emption has been extensively studied for CCS and related process algebras, it is largely ignored for mobile calculi.
The proposed research aims at studying various notions of pre-emption for the pi-calculus and at applying them for defining mechanisms for priority and real-time in this calculus. This subsumes the algebraic investigation of pre-emptive semantics and of behavioural preorders and equivalences.