Design of Complex Cyber Physical Systems with Formalized Architectural Patterns

  • Lui Sha
  • José Meseguer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5380)


The design of cyber physical systems (CPS) presents many challenges because of their complexity, strong safety requirements, distribution, and real-time nature. We propose a novel paradigm, based on the idea of using simplicity to control complexity, to achieve highly reliable CPS designs. The goal is to embody design rules of this complexity-control nature in highly reusable, very robust, and formally verified architectural patterns. We discuss some preliminary work and experiments illustrating how this can be done for CPS systems.


Architectural Pattern Logical Complexity Flight Control System Command Station Mission Duration 
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.
    Sha, L.: Using Simplicity to Control Complexity. IEEE Software (July/August 2001)Google Scholar
  2. 2.
    Lyu, M.R. (ed.): Fault Tolerance. John Wiley & Sons, Chichester (1995)Google Scholar
  3. 3.
  4. 4.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  5. 5.
  6. 6.
    Rosu, G., Havelund, K.: Rewriting-Based Techniqes for Runtime Verification. Automated Software Engineering 12, 151–197 (2005)CrossRefGoogle Scholar
  7. 7.
    Boronat, A., Meseguer, J.: An Algebraic Semantics for MOF. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 377–391. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  8. 8.
    Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161–196 (2007)CrossRefzbMATHGoogle Scholar
  9. 9.
    Behrmann, G., David, A., Larsen, K.G.: A Tutorial on UPPAAL. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  10. 10.
    Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: A Model Checker for Hybrid Systems. Softw. Tools Technol. Trans. 1, 110–122 (1997)CrossRefzbMATHGoogle Scholar
  11. 11.
    Yovine, S., Kronos: A Verification Tool for Real-Time Systems. Softw. Tools Technol. Trans. 1, 123–133 (1997)CrossRefzbMATHGoogle Scholar
  12. 12.
    Misra, J.: A Discipline of Multiprogramming. Springer, Heidelberg (2001)CrossRefzbMATHGoogle Scholar
  13. 13.
    Viswanathan, M., Viswanathan, R.: Foundations for Circular Compositional Reasoning. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 835–847. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  14. 14.
    Poernomo, I.: The meta-object facility typed. In: Proc. SAC, pp. 1845–1849. ACM, New York (2006)Google Scholar
  15. 15.
    Romero, J.R., Rivera, J.E., Duran, F., Vallecillo, A.: Formal and Tool Support for Model Driven Engineering with Maude. Journal of Object Technology 6(9) (2007)Google Scholar
  16. 16.
    Lyu, M.: Software Fault Tolerance,
  17. 17.
    Yeh, Y.C.: Dependability of the 777 Primary Flight Control System. In: Proc. Dependable Computing for Critical Applications. IEEE CS Press, Los Alamitos (1995)Google Scholar
  18. 18.
    Tyrrell, A.M., Tyrrell, A.M.: Recovery Blocks and Algorithm-Based Fault Tolerance. In: Proceedings of the 22nd EUROMICRO ConferenceGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Lui Sha
    • 1
  • José Meseguer
    • 1
  1. 1.University of Illinois at Urbana-ChampaignUSA

Personalised recommendations