A Constrained Interface Refinement Method

for

Embedded System Design

Michael G. Holland

Department of Computing, MPCE,

Macquarie University,

Sydney, NSW 2109,

Australia.

email: [email protected]

Report No. C/TR97-09

1st June, 1997

Abstract

This report presents a constrained interface approach to embedded system design. It traces the development of the Timed Transition Model (TTM) and proposes a higher level of abstraction, based on that model, that we call a Timed Transition Interface Model (TTIM). This model is the thread linking a method of hierarchical refinement, referred to here as Higher Order Embedded System Design (HOESD), and its constituent module TTMs. HOESD can be described as a dual model approach. TTIMs provide the abstraction required for reasoning about discrete-event processes at the observable interface level. A finer level of granularity, for reasoning about the functioning of individual processes themselves, is provided by the underlying module TTMs. HOESD design rules are developed, that constrain the relationship between a controller and its control environment, at each level of refinement, to comply with the top level interface specification. The leaf nodes of the design are based on provably correct constructs. Leaf node module combination is constrained, by axioms, to conform to the next higher specification level, which is thus also provably correct. This argument can be followed inductively up to the top level of specification, making the design provably correct. A mechanical process of timing analysis, which can be automated, is carried out to confirm, or deny, conformance. HOESD, as defined here, is an axiomatic approach to embedded system design, that draws from the method of Higher Order Software (HOS), developed by Hamilton & Zeldin, but uses a TTIM, rather than a functional model. TTIM is an abstraction, that draws from Ostroff's (1989) TTMs.

Keywords conformance, dynamic timing analysis, higher order embedded system design, higher order software, static timing analysis, timed transition, timed transition interface model, timed transition model.