Grant: Discovery Grants Program - Individual

Software verification is more or less an empirical process in today's industrial practice: Tests are applied to software in the hope that these tests cover most of the functionality and thus discover most (but certainly not all) of the bugs. Another approach is conformance testing (our interest): A piece of software is checked against a formal model (the specification) in a fully automated (and efficient) manner. In a first variant (model checking), the specification consists in a logical formula, which is checked against the implementation; in a second variant (model-based testing) the specification takes an algebraic form and is then compared with the implementation either directly or via systematic test suites. We note that the way we express the specification takes either a logical, or an algebraic, but never a mixed form. However, a mixed approach is often the best way to go in practice. We plan to continue recent work to unify the two variants, and so to induce practical applications of mixed specifications in the area of real-time systems (systems in which correctness implies not only correct output but also correct timing of the output). We also note that current conformance testing methods are based on finite state techniques. This is adequate for verification of hardware and communication protocols, but less so for complex application software. A second direction of our research is thus the investigation of conformance testing with context-free techniques. Real-time systems are ubiquitous nowadays, from traffic light controllers to the fly-by-wire systems found in all the commercial airliners. Often their misbehavior leads to loss of property and/or life. Our investigation into finite-state real-time conformance testing will ease the adoption of such techniques in industry; this will eventually lead to more and more robust implementations of often critical computing systems. Our investigation of context-free conformance testing will extend the above benefits to a wider range of software systems; our research has the potential of eventually eliminating the dreaded Blue Screen of Death from our desktop machines and - most importantly - from critical computing systems.