Compositional Modeling in Metropolis
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 non-trivial example, a micro-kernel real-time operating system, TinyOS.
KeywordsSchedule Policy Compositional Modeling Parallel Composition Priority Order Priority Function
Unable to display preview. Download preview PDF.
- 4.F. Balarin, L. Lavagno, C. Passerone, A. Sangiovanni-Vincentelli, Y. Watanabe, and G. Yang. Concurrent execution semantics and sequential simulation algorithms for the metropolis meta-model. In Proc. CODES’02, 2002.Google Scholar
- 5.S. Bornot, G. Gössler, and J. Sifakis. On the construction of live timed systems. In S. Graf and M. Schwartzbach, editors, Proc. TACAS’00, volume 1785 of LNCS, pages 109–126. Springer-Verlag, 2000.Google Scholar
- 7.M. Bozga, J.-C. Fernandez, L. Ghirvu, S. Graf, J.-P. Krimm, and L. Mounier. IF: A validation environment for timed asynchronous systems. In E. Emerson and A. Sistla, editors, Proc. CAV’00, volume 1855 of LNCS, pages 543–547. Springer-Verlag, 2000.Google Scholar
- 8.J. Burch, R. Passerone, and A. Sangiovanni-Vincentelli. Overcoming heterophobia: Modeling concurrency in heterogeneous systems. In Proc. 2nd International Conference on Application of Concurrency to System Design, 2001.Google Scholar
- 10.D. Culler, J. Hill, P. Buonadonna, R. Szewczyk, and A. Woo. A network-centric approach to embedded software for tiny devices. In T. Henzinger and C. M. Kirsch, editors, Proc. EMSOFT’01, volume 2211 of LNCS, pages 114–130. Springer-Verlag, 2001.Google Scholar
- 11.L. de Alfaro and T. Henzinger. Interface theories for component-based design. In T. Henzinger and C. M. Kirsch, editors, Proc. EMSOFT’01, volume 2211 of LNCS, pages 148–165. Springer-Verlag, 2001.Google Scholar
- 12.G. Gössler. Compositional Modelling of Real-Time Systems — Theory and Practice. PhD thesis, Université Joseph Fourier, Grenoble, France, 2001.Google Scholar
- 13.G. Gössler. Prometheus— a compositional modeling tool for real-time systems. In P. Pettersson and S. Yovine, editors, Proc. Workshop RT-TOOLS’01. Technical report 2001-014, Uppsala University, Department of Information Technology, 2001.Google Scholar
- 15.C. Liu and J. Layland. Scheduling algorithms for multiprogramming in a hard-real-time environment. Journal of the ACM, 20(1), 1973.Google Scholar
- 16.O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for timed systems. In E. Mayr and C. Puech, editors, STACS’95, volume 900 of LNCS, pages 229–242. Springer-Verlag, 1995.Google Scholar