One of the great challenges of computer science is the development of correct programs for real applications. The most critical real applications often involve parallel processing, concurrency, and real time. These characteristics render current techniques of software engineering less effective and emphasize the need for more formal methods. Graphical Interval Logic derived from S4.3 modal logic, closely resembles the timing diagrams drawn by software engineers and, thus, is highly intuitive and easy to use. Specifications expressed graphically for concurrent systems can be parsed into an internal modal representation and submitted to a theorem prover to provide rigorous confirmation of the intended properties of a program or system design. This project will develop an experimental implementation of Graphical Interval Logic with its associated specification database, parser, and theorem prover, and will investigate the application of the logic to the verification and testing of Ada programs. The tools will be designed in consultation with industrial partners and will be evaluated by them for use in real applications.
