Compositional Modeling in Metropolis

  • Gregor Gössler
  • Alberto Sangiovanni-Vincentelli
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2491)


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.


Schedule Policy Compositional Modeling Parallel Composition Priority Order Priority Function 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    K. Altisen, G. Gössler, and J. Sifakis. Scheduler modeling based on the controller synthesis paradigm. Journal of Real-Time Systems, special issue on “control-theoretical approaches to real-time computing”, 23(1/2):55–84, 2002.zbMATHGoogle Scholar
  2. 2.
    R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    J. Baeten, J. Bergstra, and J. Klop. Syntax and defining equations for an interrupt mechanism in process algebra. Fundamenta Informaticae, IX(2):127–168, 1986.MathSciNetGoogle Scholar
  4. 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. 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
  6. 6.
    S. Bornot and J. Sifakis. An algebraic framework for urgency. Information and Computation, 163:172–202, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 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. 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
  9. 9.
    J. Camilleri and G. Winskel. CCS with priority choice. Information and Computation, 116(1):26–37, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 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. 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. 12.
    G. Gössler. Compositional Modelling of Real-Time Systems — Theory and Practice. PhD thesis, Université Joseph Fourier, Grenoble, France, 2001.Google Scholar
  13. 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
  14. 14.
    L. Lamport. Specifying concurrent program modules. ACM Trans. on Programming Languages and Systems, 5:190–222, 1983.zbMATHCrossRefGoogle Scholar
  15. 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. 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
  17. 17.
    L. Sha, R. Rajkumar, and J. Lehoczky. Priority inheritance protocols: An approach to real-time synchronization. IEEE Transactions on Computers, 39(9):1175–1185, 1990.CrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Gregor Gössler
    • 1
  • Alberto Sangiovanni-Vincentelli
    • 1
  1. 1.Dept. of EECSUniversity of California at BerkeleyUSA

Personalised recommendations