Formal methods for system integration
Mike Fourman – 25 March 1998
The rapid increase in integration level of electronic products, and the emergence of the hardware and software intellectual property marketplace, is focusing attention on significant gaps in the methodology and technology for integrating complex systems and chipsets. In this talk we outline a new approach, based on a formal representation of behaviours as relations, to the generation of interfaces connecting independent hardware blocks. To relate the system-level behaviour to 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 system-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 are working to automate this process to provide automated interface synthesis for system integration.
Back