Computerized systems are ubiquitous in modern society. They are present in our homes, cars, medical devices and various appliances. It is extremely important to ensure that these systems function without failing and work as they are intended to. This project explores basic research to ensure the correct functioning of such systems. The proposed research will contribute towards development of error free and high quality computerized systems, especially safety critical systems. It will also make it more difficult to break into systems, thus making them safer. It will lead to reduced down time of computer systems, thus yielding economic benefits as well.
This project addresses fundamental research on static as well as dynamic techniques for ensuring correct functioning of probabilistic computer systems. The project proposes novel research on model checking concurrent probabilistic programs that exhibit individual process level non-determinism. It investigates model checking of such systems under different classes of schedulers that more accurately represent the resolution of non-determinism in them. The project also proposes dynamic techniques, based on monitoring, for ensuring correctness of probabilistic systems at run time when their internal state is not directly observable. Techniques based on state estimation are proposed and will be analyzed to ensure timely detection of malfunctioning.
