An Operational Contract Framework for Heterogeneous Systems

Modern IT systems are increasingly being built by assembling components that are pre-designed or developed concurrently in a distributed manner. In this context, contracts play a vital role for ensuring interoperability of components and adherence to specifications. For the design of e.g. embedded systems, additional complexity is found in heterogeneity of components: such systems are composed of components of very different nature, e.g. mechanical or electronic. Heterogeneity adds extra complexity to systems design, as composition of heterogeneous components is generally not well-defined, hence making design and verification difficult. So far, few approaches have attempted to address heterogeneity for embedded systems, and yet none of them has demonstrated to be really effective. Meanwhile, denotational mathematical frameworks for reasoning effectively on heterogeneous composition have recently been made available in the literature, but their operational application to a contract-based design flow is still missing. In this work, we propose a heterogeneous contract theory for embedded systems build on the tag machine formalism. We introduce heterogeneous composition, refinement, dominance, and compatibility of contracts, altogether enabling a formalized and rigorous design process for heterogeneous embedded systems.