Formal Methods in Concurrent and Distributed Systems

With the widespread use of distributed and concurrent systems and with the increase in the complexity of software for such systems, it becomes important to develop various methods for ensuring the quality of concurrent software systems. This project proposes various methods for automated and semi-automated analysis and verification of concurrent and distributed systems. In particular, the project considers methods based on temporal logic model-checking for verification of concurrent systems.

Although model-checking has been applied fairly successfully for verification of quite a few real-life systems, its applicability to a wider class of practical systems has been hampered by the state explosion problem (i.e. the enormous increase in the size of the state space). In this project, symmetry based techniques are proposed to overcome the state explosion problem.

As part of the project, a model-checking system, called SMC (Symmetry based Model-Checker), has been built. This system takes a concurrent program and an incorrectness specification specified as an automaton and checks if the program has any fair computation that is accepted by the automaton. It is an on-the-fly model-checking system that exploits the symmetries existing in the concurrent program to reduce the size of the explored state space. It can be used for checking correctness of both safety and liveness properties under different notions of fairness. It has been used to verify the Fire-wire protocol (IEEE 1394, serial bus protocol) and detected some bugs in it.

The project also considers research on semi-automated and fully automated methods for verification of parameterized systems (i.e. systems with an arbitrary number of processes). In particular, it uses induction based approaches for verification of liveness properties of parameterized systems. The project developed an automated system that checks correctness of linear networks of arbitrary size. The input to this system consists of descriptions of three processes I,P,E and an automaton A. It checks if all fair computations of all linear networks of the form--- process I, followed by a finite number copies of process P, followed by process E--- satisfy the correctness specification given by A. The system terminates giving a "yes" or "no" answer, or sometimes it may not terminate. The system works by automatically generating an inductive invariant. It can be used to check both safety and liveness properties.

The project also considers customizing commercial-off-the-shelf components to individual users. It addresses the problem of \emm{under-specification}, where an off-the-shelf component does only what it claims to do, however, it claims more behaviors than it actually has and that one wishes for, some of which may render it useless. Given such an under-specified module, we propose a method to automatically synthesize some safety properties from it that would tame its ``bad" behaviors. The advantage of restricting to safety properties is that they are monitorable. The safety properties are derived using an automata-theoretic approach. We show that, when restricting to \${\omega}-regular languages, there is no maximal safety property. For this case we construct a sequence of increasingly larger safety properties. We also show how to construct an infinite-state automata that can capture safety properties contained in the original specifications. Monitroing stochastic system for violations of temporal properties are also investigated.