Advertisement

IPL: An Integration Property Language for Multi-model Cyber-physical Systems

  • Ivan Ruchkin
  • Joshua Sunshine
  • Grant Iraci
  • Bradley Schmerl
  • David Garlan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

Design and verification of modern systems requires diverse models, which often come from a variety of disciplines, and it is challenging to manage their heterogeneity – especially in the case of cyber-physical systems. To check consistency between models, recent approaches map these models to flexible static abstractions, such as architectural views. This model integration approach, however, comes at a cost of reduced expressiveness because complex behaviors of the models are abstracted away. As a result, it may be impossible to automatically verify important behavioral properties across multiple models, leaving systems vulnerable to subtle bugs. This paper introduces the Integration Property Language (IPL) that improves integration expressiveness using modular verification of properties that depend on detailed behavioral semantics while retaining the ability for static system-wide reasoning. We prove that the verification algorithm is sound and analyze its termination conditions. Furthermore, we perform a case study on a mobile robot to demonstrate IPL is practically useful and evaluate its performance.

Notes

Acknowledgments

This material is based on research sponsored by AFRL and DARPA under agreement number FA8750-16-2-0042. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of the AFRL, DARPA or the U.S. Government.

References

  1. 1.
    Mosterman, P.J., Zander, J.: Cyber-physical systems challenges: a needs analysis for collaborating embedded software systems. Softw. Syst. Model. 15(1), 5–16 (2016)CrossRefGoogle Scholar
  2. 2.
    Fitzgerald, J., Larsen, P.G., Pierce, K., Verhoef, M., Wolff, S.: Collaborative modelling and co-simulation in the development of dependable embedded systems. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 12–26. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-16265-7_2CrossRefGoogle Scholar
  3. 3.
    Valukas, A.: Report to board of directors of general motors company regarding ignition switch recalls. Jenner & Block, Technical report (2014)Google Scholar
  4. 4.
    Sztipanovits, J., Koutsoukos, X., Karsai, G., Kottenstette, N., Antsaklis, P., Gupta, V., Goodwine, B., Baras, J., Wang, S.: Toward a science of cyber-physical system integration. In: Proceedings of the IEEE (2011)Google Scholar
  5. 5.
    Alur, R.: Principles of Cyber-Physical Systems. The MIT Press, Cambridge (2015)Google Scholar
  6. 6.
    Dijkman, R.M.: Consistency in multi-viewpoint architectural design. Ph.D. thesis, Telematica Instituut, Enschede, The Netherlands (2006)Google Scholar
  7. 7.
    Maoz, S., Ringert, J.O., Rumpe, B.: Synthesis of component and connector models from crosscutting structural views. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013, New York, NY, USA, pp. 444–454. ACM (2013)Google Scholar
  8. 8.
    Reineke, J., Tripakis, S.: Basic problems in multi-view modeling. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 217–232. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54862-8_15CrossRefGoogle Scholar
  9. 9.
    Bhave, A.: Multi-view consistency in architectures for cyber-physical systems. Ph.D. thesis, Carnegie Mellon University, December 2011Google Scholar
  10. 10.
    Howard, R.A.: Dynamic Programming and Markov Processes. Technology Press of the Massachusetts Institute of Technology, Cambridge (1960)zbMATHGoogle Scholar
  11. 11.
    Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-72522-0_6CrossRefGoogle Scholar
  12. 12.
    Bhave, A., Krogh, B., Garlan, D., Schmerl, B.: View consistency in architectures for cyber-physical systems. In: IEEE/ACM International Conference on Cyber-Physical Systems (ICCPS) (2011)Google Scholar
  13. 13.
    Nuseibeh, B., Kramer, J., Finkelstein, A.: A framework for expressing the relationships between multiple views in requirements specification. IEEE Trans. Softw. Eng. 20(10), 760–773 (1994)CrossRefGoogle Scholar
  14. 14.
    Egyed, A.F.: Heterogeneous view integration and its automation. Ph.D. thesis, University of Southern California (2000)Google Scholar
  15. 15.
    Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)CrossRefGoogle Scholar
  16. 16.
    Smith, G.: The Object-Z Specification Language. Advances in Formal Methods, vol. 1. Springer, New York (2000).  https://doi.org/10.1007/978-1-4615-5265-9CrossRefzbMATHGoogle Scholar
  17. 17.
    Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)CrossRefGoogle Scholar
  18. 18.
    Karsai, G., Sztipanovits, J.: Model-integrated development of cyber-physical systems. In: Brinkschulte, U., Givargis, T., Russo, S. (eds.) SEUS 2008. LNCS, vol. 5287, pp. 46–54. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-87785-1_5CrossRefGoogle Scholar
  19. 19.
    Ruchkin, I.: Integration beyond components and models: research challenges and directions. In: Proceedings of the Third Workshop on Architecture Centric Virtual Integration (ACVI), Venice, Italy, pp. 8–11 (2016)Google Scholar
  20. 20.
    Kruchten, P.: The 4+1 view model of architecture. IEEE Softw. 12, 42–50 (1995)CrossRefGoogle Scholar
  21. 21.
    Rajhans, A., Bhave, A., Loos, S., Krogh, B., Platzer, A., Garlan, D.: Using parameters in architectural views to support heterogeneous design and verification. In: Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference (CDC) (2011)Google Scholar
  22. 22.
    Marinescu, R.: Model-driven analysis and verification of automotive embedded systems. Ph.D. thesis, Maladaren University (2016)Google Scholar
  23. 23.
    Vanherpen, K., Denil, J., David, I., De Meulenaere, P., Mosterman, P.J., Torngren, M., Qamar, A., Vangheluwe, H.: Ontological reasoning for consistency in the design of cyber-physical systems, pp. 1–8. IEEE, April 2016Google Scholar
  24. 24.
    Torngren, M., Qamar, A., Biehl, M., Loiret, F., El-khoury, J.: Integrating viewpoints in the development of mechatronic products. Mechatronics 24, 745–762 (2013)CrossRefGoogle Scholar
  25. 25.
    Rajhans, A., Krogh, B.H.: Heterogeneous verification of cyber-physical systems using behavior relations. In: Proceedings of the 15th ACM Conference on Hybrid Systems: Computation and Control (HSCC), New York, NY, USA, pp. 35–44. ACM (2012)Google Scholar
  26. 26.
    Lee, E.A., Neuendorffer, S., Zhou, G.: System Design, Modeling, and Simulation using Ptolemy II. Ptolemy.org, Berkeley (2014)Google Scholar
  27. 27.
    Combemale, B., Deantoni, J., Baudry, B., France, R., Jezequel, J.M., Gray, J.: Globalizing modeling languages. Computer 47(6), 68–71 (2014)CrossRefGoogle Scholar
  28. 28.
    Sztipanovits, J., Bapty, T., Neema, S., Howard, L., Jackson, E.: OpenMETA: a model- and component-based design tool chain for cyber-physical systems. In: Bensalem, S., Lakhneck, Y., Legay, A. (eds.) ETAPS 2014. LNCS, vol. 8415, pp. 235–248. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54848-2_16CrossRefzbMATHGoogle Scholar
  29. 29.
    Simko, G., Lindecker, D., Levendovszky, T., Neema, S., Sztipanovits, J.: Specification of cyber-physical components with formal semantics – integration and composition. In: Moreira, A., Schätz, B., Gray, J., Vallecillo, A., Clarke, P. (eds.) MODELS 2013. LNCS, vol. 8107, pp. 471–487. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-41533-3_29CrossRefGoogle Scholar
  30. 30.
    Ruchkin, I., de Niz, D., Chaki, S., Garlan, D.: Contract-based integration of cyber-physical analyses. In: Proceedings of the International Conference on Embedded Software (EMSOFT), New York, NY, USA, pp. 23:1–23:10. ACM (2014)Google Scholar
  31. 31.
    Da Costa, A., Laroussinie, F., Markey, N.: Quantified CTL: expressiveness and model checking. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 177–192. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-32940-1_14CrossRefGoogle Scholar
  32. 32.
    Borger, E., Gradel, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (2001)zbMATHGoogle Scholar
  33. 33.
    Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57, October 1977Google Scholar
  34. 34.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992).  https://doi.org/10.1007/978-1-4612-0931-7CrossRefzbMATHGoogle Scholar
  35. 35.
    Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Combination methods for satisfiability and model-checking of infinite-state systems. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 362–378. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73595-3_25CrossRefGoogle Scholar
  36. 36.
    Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: Formalizing requirements with object models and temporal constraints. Softw. Syst. Model. 10(2), 147–160 (2009)CrossRefGoogle Scholar
  37. 37.
    Gabbay, D.M.: Fibred semantics and the weaving of logics part 1: modal and intuitionistic logics. J. Symb. Log. 61(4), 1057–1120 (1996)CrossRefGoogle Scholar
  38. 38.
    Konur, S., Fisher, M., Schewe, S.: Combined model checking for temporal, probabilistic, and real-time logics. Theor. Comput. Sci. 503, 61–88 (2013)MathSciNetCrossRefGoogle Scholar
  39. 39.
    Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)MathSciNetCrossRefGoogle Scholar
  40. 40.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)CrossRefGoogle Scholar
  41. 41.
    Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)CrossRefGoogle Scholar
  42. 42.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  43. 43.
    Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  44. 44.
    Clements, P., Bachmann, F., Bass, L., Garlan, D., Ivers, J., Little, R., Merson, P., Nord, R., Stafford, J.: Documenting Software Architectures: Views and Beyond, 2nd edn. Addison-Wesley Professional, Boston (2010)Google Scholar
  45. 45.
    Gurfinkel, A., Shoham, S., Meshman, Y.: SMT-based Verification of Parameterized Systems. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, New York, NY, USA, pp. 338–348. ACM (2016)Google Scholar
  46. 46.
    Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-74105-3CrossRefzbMATHGoogle Scholar
  47. 47.
    Ruchkin, I., Sunshine, J., Iraci, G., Schmerl, B., Garlan, D.: Appendix for IPL: an integration property language for multi-model cyber-physical systems (2018). http://acme.able.cs.cmu.edu/pubs/uploads/pdf/fm2018-appendix.pdf
  48. 48.
    Yin, R.K.: Case Study Research: Design and Methods, 4th edn. Sage Publications Inc., Thousand Oaks (2008)Google Scholar
  49. 49.
    Quigley, M., Gerkey, B., Smart, W.D.: Programming Robots with ROS: A Practical Introduction to the Robot Operating System, 1st edn. O’Reilly Media, Sebastopol (2015)Google Scholar
  50. 50.
    Feiler, P.H., Gluch, D.P., Hudak, J.J.: The architecture analysis & design language (AADL): an introduction. Technical report CMU/SEI-2006-TN-011, Software Engineering Institute, Carnegie Mellon University (2006)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Ivan Ruchkin
    • 1
  • Joshua Sunshine
    • 1
  • Grant Iraci
    • 1
  • Bradley Schmerl
    • 1
  • David Garlan
    • 1
  1. 1.Institute for Software ResearchCarnegie Mellon UniversityPittsburghUSA

Personalised recommendations