Formal semantics of modular time refinement in AutoFocus

摘要

Modern automobile embedded systems form highly complex distributed networks of electronic control units (ECUs). Model-based development is a widespread approach to tackle this complexity. AutoFocus is a CASE tool prototype aiming at formally sound model-based development of embedded systems. A model is hierarchically composed of components that communicate over typed channels. AutoFocus has a robust and plain formal semantics: communication and execution are synchronised by a global clock for all components. In this article we present an extension of the AutoFocus semantics allowing time refinement of components. It enables a simpler modularisation of systems, a better structuring of behaviour specifications, and a better mapping to the target platform of real embedded systems. At the same time, it maintains the advantages of fixed clocking of the AutoFocus semantics, such as strong causality and guaranteed termination of computation steps.