B.Tech. Project Report, Department of Computer Science and Engineering, Indian Institute of Technology Bombay, May 2001.
This project considers the problem of efficient verification of synchronous programs. The underlying idea used is based upon a recent proposal: To verify a property for a system, one method would be to decompose the system into smaller subsytems, and verify local properties on each of them. We use the technique of program slicing to decompose the system into smaller subsystems. In this project, we considered two synchronous languages: Communicating Reactive State Machines (CRSMs) and Esterel. CRSMs are a paradigm based on Argos, another synchronous programming language. We have proposed an algorithm that slices Argos programs and have formally proved that it produces correct slides. This algorithm was then extended to slice CRSMs. The other part of the project considers slicing Esterel programs. An attempt has been made to extend the notion of the Control Flow Graph (CFG) and the Program Dependence Graph (PDG) for Esterel.
Project Report:
[
PDF
]
(© Vinod Ganapathy)