Compositional modeling in metropolis

Abstract

Metropolis is an environment for the design of heterogeneous embedded systems. The framework is based on a general system representation called the Metropolis meta-model. This model forms the backbone of the software system and is used to integrate a variety of analysis and synthesis tools. Compositional modeling is a powerful method for assembling components so that their composition satisfies a set of given properties thus making the verification problem much simpler to solve. We use the meta-model to integrate the Prometheus tool in Metropolis for supporting compositional modeling and verification of Metropolis specifications and present a first set of results on a nontrivial example, a micro-kernel real-time operating system, TinyOS. © Springer-Verlag Berlin Heidelberg 2002.