Formal methods

Overview

WatForm (Waterloo Formal Methods) draws its members from the Cheriton School of Computer Science and the Department of Electrical and Computer Engineering. The group uses rigorous mathematics to engineer real-world, computer-based systems, ranging from microprocessors to telephone systems. Mathematical modelling and analysis can reveal errors early in the development process, when they are easiest and cheapest to correct.

Digital-system designers rely on a hierarchy of abstractions, ranging from switch-level models to instruction-set architectures, to treat collections of transistors as single modules. Missing is an abstraction level between the register-transfer level and the functional-block level. The group is developing a theory of the structure and behaviour at the pipeline level, which will make design and validation more systematic, thorough, and productive. Using this theory, the group is investigating ways of verifying high-performance microprocessors with complex optimizations, such as out-of-order and superscalar execution.

The rising complexity of automatic control systems poses problems of formal verification and synthesis. Modern automation requires not only the design of small-scale feedback loops, but also the co-ordination of large numbers of interacting subsystems. The group is devising analysis and synthesis methods for large-scale discrete-event control systems.

The feature interaction problem is prevalent in software systems in which features are developed as independent extensions to the same application, when in fact the features subtly interfere with each other with respect to shared data. The group is investigating ways to detect interactions, and to preserve modular development of features by resolving interactions via verified coordination models and synthesized controllers.

A common challenge for all of these applications is the need for requirements notations that are readable and configurable, but still formal. WatForm members are investigating practical requirements notations and techniques for supporting configurable model-driven development such as the automatic creation of code generators, simulators, and model checkers for these notations.

The group has close contacts with industry and receives funding from NSERC, CFI, CITO (OCE), Bell University Labs, General Motors of Canada, Intel, Nortel Networks, and the Semiconductor Research Corporation (SRC).