Grant: Discovery Grants Program - Individual

An ""interface contract"" is a formal definition of what constitutes a valid interaction with a particular system over time. For example, a web browser running an application such as Facebook sends commands to the Facebook server and processes its responses to update its display. Similar to a real-world contract between two people, the interface contract clearly defines how the browser and the server are expected to converse with each other: which commands can be sent, what responses are expected, and even what values can be put into the various commands. Not following the contract by either side can result in the other side being thrown into an unexpected state. Similarly, the testing of spacecraft systems for the future Martian rovers involves the execution of thousands of commands and responses. These sequences of events are then searched for violations of a ""contract"" that hints at component malfunction. Although not explicitly called as such, interface contracts are present in a wide variety of software systems. However, very little tools are available for developers and users to ensure contract compliance between communicating ""peers"". The proposed research program concentrates on the application of formal methods to software engineering. In particular, it aims to model, verify and enforce valid sequences of events generated by systems through the use of mathematical logic. Practical solutions to these problems present a potential of direct application in a wide range of domains. In term, a comprehensive analysis of trace validation and monitoring, taking into account sequential and data dependencies in interface contracts, could produce useful development, debugging and testing tools, and improve the safety and reliability of software systems.