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 static as well as runtime verification of such computer systems.

As part of the static verification, the project investigates model checking based methods for analysis and verification. It explores such methods for deterministic as well as probabilistic systems.

As part of the run time verification, project develops methods for detecting faults at execution time when the faults are specified on the underlying computations of the system in expressive languages such as temporal logic and automata. The developed methods are used for safe deployment and operation of Cyber Physical Systems such as Autonomous cars, Home assist robots, etc. The project employs Hidden Markov Models for capturing the behavior of such systems and develops accurate and timely monitors for detecting erroneous behavior in such systems.