Masaccio: A Formal Model for Embedded Components

Masaccio is a formal model for hybrid dynamical systems which are built from atomic discrete components (di erence equations) and atomic continuous components (di erential equations) by parallel and serial composition, arbitrarily nested. Each system component consists of an interface, which determines the possible ways of using the component, and a set of executions, which de ne the possible behaviors of the component in real time. We formally de ne a class of entities called \components." The intended use of components is to provide a formal, structured model for software and hardware that interacts with a physical environment in real time. The model is formal in that it de nes a component as a mathematical object, which can be analyzed. The model is structured in that it permits the hierarchical de nition of a component, and the hierarchy can be exploited for structuring the analysis. Components are built from atomic components using six operations: parallel composition, serial...

• Type: Conference
• Year: 2000
• Where: IFIPTCS
• Authors: Thomas A. Henzinger
• Keywords: Atomic Continuous Component, Atomic Discrete Component, Di Erence Equation, IFIPTCS 2000, Theoretical Computer Science