Skip to main content
SpringerLink
Log in
Book cover

Transactions on Foundations for Mastering Change I pp 113–129Cite as

Compositional Model-Based System Design and Other Foundations for Mastering Change

  • Chapter
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((TFMC,volume 9960))

Abstract

The topic of this paper is the design of dynamical systems, such as embedded or cyber-physical systems. Is there a science of system design, and if so, what are its elements? We believe that its key elements are three: modeling, analysis, and implementation, and we discuss fundamental research challenges in each category. We then argue that compositionality is an essential cross-cutting concern, and one of the foundations for mastering change. Beyond compositionality, we discuss other key problems when dealing with change, namely, multi-view modeling and synthesis.

This work was partially supported by the Academy of Finland and the U.S. National Science Foundation (awards #1329759 and #1139138). Technical details of the works the author has been involved in can be found in the referenced papers, as well as in more pedagogical forms in [Tri15b, Tri16].

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    One may argue that static systems are just a special case of dynamical systems, where the dynamics is trivial: the state never changes.

References

  1. Alur, R., Henzinger, T.: Reactive modules. Formal Methods Syst. Des. 15, 7–48 (1999)

    Article  Google Scholar 

  2. Alur, R., Martin, M., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Synthesizing finite-state protocols from scenarios and requirements. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 75–91. Springer, Heidelberg (2014). doi:10.1007/978-3-319-13338-6_7

    Google Scholar 

  3. Angluin, D.: Computational learning theory: survey and selected bibliography. In: 24th Annual ACM Symposium on Theory of Computing, pp. 351–369 (1992)

    Google Scholar 

  4. Alur, R., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Automatic completion of distributed protocols with symmetry. In: 27th International Conference on Computer Aided Verification (CAV), pp. 395–412 (2015)

    Google Scholar 

  5. Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification - specification is the new bottleneck. In: 7th Conference on Systems Software Verification, SSV 2012, Sydney, Australia, pp. 18–32, 28–30 November 2012

    Google Scholar 

  6. Broman, D., Brooks, C., Greenberg, L., Lee, E.A., Tripakis, S., Wetter, M., Masin, M.: Determinate composition of FMUs for co-simulation. In: 13th ACM & IEEE International Conference on Embedded Software (EMSOFT 2013) (2013)

    Google Scholar 

  7. Bertolino, A., Calabrò, A., Merten, M., Steffen, B.: Never-stop learning: continuous validation of learned models for evolving systems through monitoring. ERCIM News 88, 2012 (2012)

    Google Scholar 

  8. Bogomolov, S., Greitschus, M., Jensen, P.G., Larsen, K.G., Mikucionis, M., Strump, T., Tripakis, S.: Co-simulation of hybrid systems with SpaceEx and Uppaal. In: Proceedings of the 11th International Modelica Conference. Linkoping University Electronic Press (2015)

    Google Scholar 

  9. Broman, D., Greenberg, L., Lee, E.A., Masin, M., Tripakis, S., Wetter, M., Requirements for hybrid cosimulation standards. In: Hybrid Systems: Computation and Control (HSCC 2015) (2015)

    Google Scholar 

  10. Beckert, B., Hähnle, R.: Reasoning and verification: state of the art and current trends. IEEE Intell. Syst. 29(1), 20–29 (2014)

    Article  Google Scholar 

  11. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  12. Bilitchenko, L., Liu, A., Cheung, S., Weeding, E., Xia, B., Leguia, M., Anderson, J.C., Densmore, D.: Eugene - a domain specific language for specifying and constraining synthetic biological parts, devices, and systems. PLoS ONE 6(4), e18882 (2011)

    Article  Google Scholar 

  13. Broman, D., Lee, E.A., Tripakis, S., Törngren, M.: Viewpoints, formalisms, languages, and tools for cyber-physical systems. In: 6th International Workshop on Multi-Paradigm Modeling (MPM 2012) (2012)

    Google Scholar 

  14. Blochwitz, T., Otter, M., Åkesson, J., Arnold, M., Clauss, C., Elmqvist, H., Friedrich, M., Junghanns, A., Mauss, J., Neumerkel, D., Olsson, H., Viel, A.: Functional mockup interface 2.0: the standard for tool independent exchange of simulation models. In: 9th International Modelica Conference (2012)

    Google Scholar 

  15. Broy, M., Stølen, K.: Specification, Development of Interactive Systems: Focus On Streams, Interfaces and Refinement. Springer, Heidelberg (2001)

    Book  MATH  Google Scholar 

  16. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM Symposium on POPL (1977)

    Google Scholar 

  17. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  18. Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Learning extended finite state machines. In: Software Engineering and Formal Methods - SEFM, pp. 250–264 (2014)

    Google Scholar 

  19. Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: Fourth Annual Symposium on Logic in Computer Science (1989)

    Google Scholar 

  20. Cremona, F., Lohstroh, M., Tripakis, S., Brooks, C., Lee, E.A.: FIDE - an FMI integrated development environment. In: 31st ACM/SIGApp. Symposium on Applied Computing, Embedded Systems Track (SAC) (2016)

    Google Scholar 

  21. Caspi, P., Scaife, N., Sofronis, C., Tripakis, S.: Semantics-preserving multitask implementation of synchronous programs. ACM Trans. Embed. Comput. Syst. (TECS) 7(2), 1–40 (2008)

    Article  Google Scholar 

  22. de Alfaro, L., Henzinger, T.: Interface automata. In: Foundations of Software Engineering (FSE). ACM Press (2001)

    Google Scholar 

  23. Dill, D.L.: Trace theory for automatic hierarchical verification of speed-independent circuits. MIT Press, Cambridge (1987)

    Google Scholar 

  24. Dragomir, I., Preoteasa, V., Tripakis, S.: Compositional semantics and analysis of hierarchical block diagrams. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 38–56. Springer, Heidelberg (2016). doi:10.1007/978-3-319-32582-8_3

    Chapter  Google Scholar 

  25. Eker, J., Janneck, J., Lee, E., Liu, J., Liu, X., Ludvig, J., Neuendorffer, S., Sachs, S., Xiong, Y.: Taming heterogeneity - the Ptolemy approach. Proc. IEEE 91(1), 127–144 (2003)

    Article  Google Scholar 

  26. Fisher, J., Henzinger, T.A.: Executable biology. In: Winter Simulation Conference, pp. 1675–1682 (2006)

    Google Scholar 

  27. Fu, J., Topcu, U.: Probably approximately correct MDP learning and control with temporal logic constraints. CoRR, abs/1404.7073 (2014)

    Google Scholar 

  28. Governatori, G., Milosevic, Z.: Dealing with contract violations: formalism and domain specific language. In: 2005 Ninth IEEE International EDOC Enterprise Computing Conference, pp. 46–57, September 2005

    Google Scholar 

  29. Giantamidis, G., Tripakis, S.: Learning Moore Machines from Input-Output Traces. ArXiv e-prints, May 2016

    Google Scholar 

  30. Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pp. 317–330. ACM, New York (2011)

    Google Scholar 

  31. Gulwani, S.: Synthesis from examples: interaction models and algorithms. In: Proceedings of the 2012 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012, pp. 8–14. IEEE Computer Society, Washington (2012)

    Google Scholar 

  32. Harel, D.: Can programming be liberated, period? Computer 41(1), 28–37 (2008)

    Article  Google Scholar 

  33. Henzinger, T.A., Qadeer, S., Rajamani, S.K.: You assume, we guarantee: methodology and case studies. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 440–451. Springer, Heidelberg (1998). doi:10.1007/BFb0028765

    Chapter  Google Scholar 

  34. Howar, F., Steffen, B.: Learning models for verification and testing - special track at ISoLA 2014 track introduction. In: Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, pp. 199–201 (2014)

    Google Scholar 

  35. Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011). doi:10.1007/978-3-642-25271-6_8

    Chapter  Google Scholar 

  36. Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: sel4: Formal verification of an operating-system kernel. Commun. ACM 53(6), 107–115 (2010)

    Article  Google Scholar 

  37. Kaivola, R., Ghughal, R., Narasimhan, N., Telfer, A., Whittemore, J., Pandav, S., Slobodová, A., Taylor, C., Frolov, V., Reeber, E., Naik, A.: Replacing testing with formal verification in intel core TM i7 processor execution engine validation. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 414–429. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_32

    Chapter  Google Scholar 

  38. Kim, K.-D., Kumar, P.R.: Cyber-physical systems: a perspective at the centennial. Proc. IEEE 100(Special Centennial Issue), 1287–1308 (2012)

    Article  Google Scholar 

  39. Lee, E.A.:Cyber physical systems: design challenges. In: 2008 11th IEEE International Symposium on Object Oriented Real-Time Distributed Computing (ISORC), pp. 363–369, May 2008

    Google Scholar 

  40. Lublinerman, R., Szegedy, C., Tripakis, S.: Modular code generation from synchronous block diagrams - modularity vs. code size. In: 36th ACM Symposium on Principles of Programming Languages (POPL 2009), pp. 78–89. ACM (2009)

    Google Scholar 

  41. Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Q. 2, 219–246 (1989)

    MathSciNet  MATH  Google Scholar 

  42. Lamouchi, H., Thistle, J.: Effective control synthesis for DES under partial observations. In: 39th IEEE Conference on Decision and Control, pp. 22–28 (2000)

    Google Scholar 

  43. Lublinerman, R., Tripakis, S.: Modularity vs. reusability: code generation from synchronous block diagrams. In: Design, Automation, and Test in Europe (DATE 2008), pp. 1504–1509. ACM, March 2008

    Google Scholar 

  44. Leino, K.R.M., Wüstholz, V.: The dafny integrated development environment. In: 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, 6 April 2014, EPTCS, vol. 149, pp. 3–15 (2014)

    Google Scholar 

  45. Meyer, B.: Applying “Design by Contract". Computer 25(10), 40–51 (1992)

    Article  Google Scholar 

  46. Mitra, S., Wongpiromsarn, T., Murray, R.M.: Verifying cyber-physical interactions in safety-critical systems. IEEE Secur. Priv. 11(4), 28–37 (2013)

    Article  Google Scholar 

  47. Nicolescu, G., Mosterman, P.J.: Model-Based Design for Embedded Systems. CRC Press, Boston (2009)

    Book  Google Scholar 

  48. Neskovic, S., Paunovic, O., Babarogic, S.: Using protocols and domain specific languages to achieve compliance of administrative processes with legislation. In: Electronic Government and the Information Systems Perspective, EGOVIS, pp. 284–298 (2011)

    Google Scholar 

  49. Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How amazon web services uses formal methods. Commun. ACM 58(4), 66–73 (2015)

    Article  Google Scholar 

  50. Namjoshi, K.S., Trefler, R.J.: On the completeness of compositional reasoning methods. ACM Trans. Comput. Logic 11(3), 16 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  51. Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K. (ed.) Logics, Models of Concurrent Systems. Sub-series F: Computer and System Science, pp. 123–144. Springer, Heidelberg (1985)

    Chapter  Google Scholar 

  52. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: ACM Symposium, POPL (1989)

    Google Scholar 

  53. Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proceedings of the 31th IEEE Symposium on Foundations of Computer Science, pp. 746–757 (1990)

    Google Scholar 

  54. Preoteasa, V., Tripakis, S.: Refinement calculus of reactive systems. In: Proceedings of the 14th ACM & IEEE International Conference on Embedded Software (EMSOFT 2014) (2014)

    Google Scholar 

  55. Pittou, M., Tripakis, S.: Multi-view consistency for infinitary regular languages. Infect Dis. Ther. 3(1), 35–43 (2011). International Conference on Embedded Computer Systems: Observation of strains. Architectures, Modeling and Simulation - SAMOS XVI, 2016

    Google Scholar 

  56. Preoteasa, V., Tripakis, S.: Towards compositional feedback in non-deterministic and non-input-receptive systems. In: 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2016)

    Google Scholar 

  57. Rajkumar, R., Lee, I., Sha, L., Stankovic, J.: Cyber-physical systems: the next computing revolution. In: 2010 47th ACM/IEEE Design Automation Conference (DAC), pp. 731–736, June 2010

    Google Scholar 

  58. Reineke, J., Stergiou, C., Tripakis, S.: Basic problems in multi-view modeling (2016). Submitted journal version of [59]

    Google Scholar 

  59. Reineke, J., Tripakis, S.: Basic problems in multi-view modeling. In: Tools and Algorithms for the Construction and Analysis of Systems - TACAS (2014)

    Google Scholar 

  60. Raychev, V., Vechev, M.T., Yahav, E.: Code completion with statistical language models. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, p. 44 (2014)

    Google Scholar 

  61. Ramadge, P., Wonham, W.: The control of discrete event systems. Proc. IEEE 77(1), 81–98 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  62. Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. MIT Press, Cambridge (1998)

    Google Scholar 

  63. Shin, I., Lee, I.: Compositional real-time scheduling framework. ACM Trans. Embed. Comput. Syst. (TECS) 7(3), 30 (2008)

    Google Scholar 

  64. Solar-Lezama, A., Rabbah, R., Bodík, R., Ebcioğlu, K.: Programming by sketching for bit-streaming programs. SIGPLAN Not. 40(6), 281–294 (2005)

    Article  Google Scholar 

  65. Steffen, B.: LNCS transaction on the foundations for mastering change: preliminary manifesto. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. Part I. LNCS, vol. 8802, pp. 514–517. Springer, Heidelberg (2014)

    Google Scholar 

  66. Thiele, L., Chakraborty, S., Naedele, M.: Real-time calculus for scheduling hard real-time systems. In: Circuits and Systems, ISCAS (2000)

    Google Scholar 

  67. Tripakis, S., Dang, T.: Modeling, verification and testing using timed and hybrid automata. In: Mosterman, P., Nicolescu, G. (eds.) Model-Based Design for Embedded Systems. CRC Press, Boca Raton (2009)

    Google Scholar 

  68. Thistle, J.G.: Supervisory control of discrete event systems. Math. Comput. Model. 23(11/12), 25–53 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  69. Tripakis, S., Lickly, B., Henzinger, T.A., Lee, E.A.: A theory of synchronous relational interfaces. ACM Trans. Program. Lang. Syst. (TOPLAS) 33(4), 14 (2011)

    Article  Google Scholar 

  70. Tripakis, S., Limaye, R., Ravindran, K., Wang, G., Andrade, H., Ghosal, A.: Tokens vs. signals: on conformance between formal models of dataflow and hardware. J. Sig. Process. Syst. 85(1), 23–43 (2016)

    Article  Google Scholar 

  71. Tripakis, S., Pinello, C., Benveniste, A., Sangiovanni-Vincentelli, A., Caspi, P., Di Natale, M.: Implementing synchronous models on loosely time-triggered architectures. IEEE Trans. Comput. 57(10), 1300–1314 (2008)

    Article  MathSciNet  Google Scholar 

  72. Tripakis, S.: Undecidable problems of decentralized observation and control on regular languages. Inf. Process. Lett. 90(1), 21–28 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  73. Tripakis, S.: Bridging the semantic gap between heterogeneous modeling formalisms, FMI. Infect Dis. Ther. 3(1), 35–43 (2011). International Conference on Embedded Computer Systems: Observation of Strains, Architectures, Modeling and Simulation - SAMOS XV, 2015

    Google Scholar 

  74. Tripakis, S.: Foundations of compositional model-based system design. In: Rawat, D.B., Rodrigues, J., Stojmenovic, I. (eds.) Cyber-Physical Systems: Observation of strains: From Theory to Practice. CRC Press, Boca Raton (2011). Infect Dis Ther. 3(1), 35–43 (2015)

    Google Scholar 

  75. Tripakis, S.: Compositionality in the science of system design. Proc. IEEE 104(5), 960–972 (2016)

    Article  Google Scholar 

  76. Tripakis, S., Stergiou, C., Shaver, C., Lee, E.A.: A modular formal semantics for Ptolemy. Math. Struct. Comput. Sci. 23, 834–881 (2013)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Aalto University, Espoo, Finland

    Stavros Tripakis

  2. University of California, Berkeley, USA

    Stavros Tripakis

Authors
  1. Stavros Tripakis
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Stavros Tripakis .

Editor information

Editors and Affiliations

  1. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this chapter

Cite this chapter

Tripakis, S. (2016). Compositional Model-Based System Design and Other Foundations for Mastering Change. In: Steffen, B. (eds) Transactions on Foundations for Mastering Change I. Lecture Notes in Computer Science(), vol 9960. Springer, Cham. https://doi.org/10.1007/978-3-319-46508-1_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46508-1_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46507-4

  • Online ISBN: 978-3-319-46508-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation