Compositional Architecture for Simple Design Formally Specified in DESIRE

摘要

A simple generic design task is described whereafter a simple scheduling task is described as a specific instance of it. A concise description of DESIRE, a framework for specification of compositional architectures, is presented. It is demonstrated how a generic compositional architecture for simple design can be formally specified by means of DESIRE and how an architecture for simple scheduling can be specified as an instantiation of the generic specification. The reasoning behavior of the resulting architecture is elucidated by reasoning trace. The full specification of the scheduling architecture is included as the appendix.