Formal Methods for System Integration

Abstract

In this talk we outline a new approach to the generation of interfaces connecting independent hardware blocks. Our treatment is based on the formal representation of synchronous behaviours as relations. To relate the behaviours of encapsulated components, we model and relate behaviours at different levels of abstraction.

We base our presentation on a small, but revealing, case study; starting from a high-level specification, we design a digital stopclock. The stopclock is specified, and designed, in terms of user-level time ticks, and is implemented in terms of a much faster implementation-level clock. A block diagram of the design is formalised at the abstract level. Abstractions are introduced to relate this to the low-level implementation. The interface logic, necessary to connect components using different abstractions, is formally derived.

We propose to automate this process to provide automated interface synthesis for system integration.

Transparencies