Top

Published in:

2024 | OriginalPaper | Chapter

Formal Model Engineering of Distributed CPSs Using AADL: From Behavioral AADL Models to Multirate Hybrid Synchronous AADL

Authors : Kyungmin Bae, Peter Csaba Ölveczky

Published in: Formal Aspects of Component Software

Publisher: Springer Nature Switzerland

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

A promising way of integrating formal methods into industrial system design is to endow industrial modeling tools with automatic formal analyses. In this paper we identify some challenges for providing such formal methods “backends” for cyber-physical systems (CPSs), and argue that Maude could meet these challenges. We then give an overview of our research on integrating Maude analysis into the OSATE tool environment for the industrial CPS modeling standard AADL.

Since many critical distributed CPSs are “logically synchronous,” a key feature making automatic formal analysis practical is the use of synchronizers for CPSs. We identify a sublanguage of AADL to describe synchronous CPS designs. We can then use Maude to effectively verify such synchronous designs, which under certain conditions also verifies the corresponding asynchronous distributed systems, with clock skews and communication delays. We then explain how we have extended our methods to multirate systems and to CPSs with continuous behaviors.

We illustrate the effectiveness of Maude-based formal model engineering of industrial CPSs on avionics control systems and collections of drones. Finally, we identify future directions in this line of research.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter From Reversible Computation to Checkpoint-Based Rollback Recovery for Message-Passing Concurrent Programs

next chapter Challenges Engaging Formal CBSE in Industrial Applications

We do not have space to discuss related work in this overview paper, but our papers have extensive discussions of related work that justify our claims.

Abrial, J.-R., Börger, E., Langmaack, H. (eds.): Formal Methods for Industrial Applications. LNCS, vol. 1165. Springer, Heidelberg (1996). https://doi.org/10.1007/BFb0027227CrossRef

Al-Nayeem, A., Sha, L., Cofer, D.D., Miller, S.M.: Pattern-based composition and analysis of virtually synchronized real-time distributed systems. In: 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems, pp. 65–74. IEEE (2012)

Al-Nayeem, A., Sun, M., Qiu, X., Sha, L., Miller, S.P., Cofer, D.D.: A formal architecture pattern for real-time distributed systems. In: Proceedings of RTSS, pp. 161–170. IEEE, USA (2009)

AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386–392. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22944-2_28CrossRef

Arias, J., Bae, K., Olarte, C., Ölveczky, P.C., Petrucci, L., Rømming, F.: Rewriting logic semantics and symbolic analysis for parametric timed automata. In: 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2022), pp. 3–15. ACM (2022)

Arias, J., Bae, K., Olarte, C., Ölveczky, P.C., Petrucci, L., Rømming, F.: Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving. In: Gomes, L., Lorenz, R. (eds.) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2023. LNCS, vol. 13929. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-33620-1_20

Arney, D., Jetley, R., Jones, P., Lee, I., Sokolsky, O.: Formal methods based development of a PCA infusion pump reference model: Generic infusion pump (GIP) project. In: HCMDSS-MDPnP, pp. 23–33. IEEE (2007)

Bae, K., Ölveczky, P.C., Feng, T.H., Tripakis, S.: Verifying Ptolemy II discrete-event models using Real-Time Maude. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 717–736. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10373-5_37CrossRef

Bae, K., Krisiloff, J., Meseguer, J., Ölveczky, P.C.: Designing and verifying distributed cyber-physical systems using Multirate PALS: an airplane turning control system case study. Sci. Comput. Program. 103, 13–50 (2015)CrossRef

10.

Bae, K., Lee, J.: Bounded model checking of signal temporal logic properties using syntactic separation. Proc. ACM Program. Lang. 3(POPL), 1–30 (2019)

11.

Bae, K., Meseguer, J., Ölveczky, P.C.: Formal patterns for multi-rate distributed real-time systems. In: Păsăreanu, C.S., Salaün, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 1–18. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35861-6_1CrossRef

12.

Bae, K., Meseguer, J., Ölveczky, P.C.: Formal patterns for multirate distributed real-time systems. Sci. Comput. Program. 91, 3–44 (2014)CrossRef

13.

Bae, K., Ölveczky, P.C.: MSYNC: a generalized formal design pattern for virtually synchronous multirate cyber-physical systems. ACM Trans. Embed. Comput. Syst. (TECS) 20(5s), 1–26 (2021)CrossRef

14.

Bae, K., Ölveczky, P.C., Al-Nayeem, A., Meseguer, J.: Synchronous AADL and its formal analysis in Real-Time Maude. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 651–667. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24559-6_43CrossRef

15.

Bae, K., Ölveczky, P.C., Feng, T.H., Lee, E.A., Tripakis, S.: Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude. Sci. Comput. Program. 77(12), 1235–1271 (2012)CrossRef

16.

Bae, K., Ölveczky, P.C., Kong, S., Gao, S., Clarke, E.M.: SMT-based analysis of virtually synchronous distributed hybrid systems. In: Proceedings of HSCC, pp. 145–154. ACM, New York, NY, USA (2016)

17.

Bae, K., Ölveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of Multirate Synchronous AADL. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 94–109. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06410-9_7CrossRef

18.

Bae, K., Ölveczky, P.C., Meseguer, J., Al-Nayeem, A.: The SynchAADL2Maude tool. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 59–62. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28872-2_4CrossRef

19.

Bae, K., Rocha, C.: Guarded terms for rewriting modulo SMT. In: Proença, J., Lumpe, M. (eds.) FACS 2017. LNCS, vol. 10487, pp. 78–97. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68034-7_5CrossRef

20.

Bae, K., Rocha, C.: Symbolic state space reduction with guarded terms for rewriting modulo SMT. Sci. Comput. Program. 178, 20–42 (2019)CrossRef

21.

Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14CrossRef

22.

Barrett, C., Stump, A., Tinelli, C., et al.: The SMT-LIB standard: Version 2.0. In: SMT. vol. 13, p. 14 (2010)

23.

Baudart, G., Benveniste, A., Bourke, T.: Loosely time-triggered architectures: improvements and comparisons. ACM Trans. Embed. Comput. Syst. (TECS) 15(4), 1–26 (2016)CrossRef

24.

Bozzano, M., Bruintjes, H., Cimatti, A., Katoen, J.-P., Noll, T., Tonetta, S.: Formal methods for aerospace systems. In: Nakajima, S., Talpin, J.-P., Toyoshima, M., Yu, H. (eds.) Cyber-Physical System Design from an Architecture Analysis Viewpoint, pp. 133–159. Springer, Singapore (2017). https://doi.org/10.1007/978-981-10-4436-6_6CrossRef

25.

Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_18CrossRef

26.

Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 52–67. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_4CrossRef

27.

Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1CrossRef

28.

Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_49CrossRef

29.

Eidson, J.: https://www.nist.gov/document/tutorial-basicpdf/ (2005). Accessed 16 Jul 2023

30.

Eidson, J.C., Fischer, M., White, J.: IEEE-1588™ standard for a precision clock synchronization protocol for networked measurement and control systems. In: Proceedings of the 34th Annual Precise Time and Time Interval Systems and Applications Meeting, pp. 243–254 (2002)

31.

Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis and Design Language. Addison-Wesley, USA (2012)

32.

França, R., Bodeveix, J.P., Filali, M., Rolland, J.F., Chemouil, D., Thomas, D.: The AADL Behaviour Annex - experiments and roadmap. In: Proceedings of ICECCS 2007. IEEE, USA (2007)

33.

Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_30CrossRef

34.

Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208–214. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_14CrossRef

35.

Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret. Comput. Sci. 105, 217–273 (1992)MathSciNetCrossRef

36.

Kim, C., Sun, M., Mohan, S., Yun, H., Sha, L., Abdelzaher, T.F.: A framework for the safe interoperability of medical devices in the presence of network failures. In: ICCPS, pp. 149–158 (2010)

37.

Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \(\delta \)-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200–205. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_15CrossRef

38.

Kopetz, H., Bauer, G.: The time-triggered architecture. Proc. IEEE 91(1), 112–126 (2003)CrossRef

39.

Lee, J., Bae, K., Ölveczky, P.C.: An extension of HybridSynchAADL and its application to collaborating autonomous UAVs. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning. ISoLA 2022. LNCS, vol. 13703. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-19759-8_4

40.

Lee, J., Bae, K., Ölveczky, P.C., Kim, S., Kang, M.: Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL. Int. J. Softw. Tools Technol. Transfer 24(6), 911–948 (2022)CrossRef

41.

Lee, J., Kim, S., Bae, K., Ölveczky, P.C.: Hybrid SynchAADL: modeling and formal analysis of virtually synchronous CPSs in AADL. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 491–504. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-81685-8_23CrossRef

42.

Lee, J., Yu, G., Bae, K.: Efficient SMT-based model checking for signal temporal logic. In: 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 343–354. IEEE (2021)

43.

Leen, G., Heffernan, D., Dunne, A.: Digital networks in the automotive vehicle. Comput. Control Eng. J. 10(6), 257–266 (1999)CrossRef

44.

Lepri, D., Ábrahám, E., Ölveczky, P.C.: Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories. Sci. Comput. Program. 99, 128–192 (2015)CrossRef

45.

Liu, S., Meseguer, J., Ölveczky, P.C., Zhang, M., Basin, D.: Bridging the semantic gap between qualitative and quantitative models of distributed systems. Proc. ACM Program. Lang. 6(OOPSLA2), 315–344 (2022)CrossRef

46.

Liu, S., Ölveczky, P.C., Meseguer, J.: Modeling and analyzing mobile ad hoc networks in Real-Time Maude. J. Log. Algebraic Methods Program. 85(1), 34–66 (2016). https://doi.org/10.1016/j.jlamp.2015.05.002MathSciNetCrossRef

47.

Mavridou, A., Stachtiari, E., Bliudze, S., Ivanov, A., Katsaros, P., Sifakis, J.: Architecture-based design: a satellite on-board software case study. In: Kouchnarenko, O., Khosravi, R. (eds.) FACS 2016. LNCS, vol. 10231, pp. 260–279. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57666-4_16CrossRef

48.

Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96(1), 73–155 (1992)MathSciNetCrossRef

49.

Meseguer, J.: Taming distributed system complexity through formal patterns. In: Arbab, F., Ölveczky, P.C. (eds.) FACS 2011. LNCS, vol. 7253, pp. 1–2. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35743-5_1CrossRef

50.

Meseguer, J.: Twenty years of rewriting logic. J. Logic Algebraic Program. 81(7), 721–781 (2012)MathSciNetCrossRef

51.

Meseguer, J.: Taming distributed system complexity through formal patterns. Sci. Comput. Program. 83, 3–34 (2014)CrossRef

52.

Meseguer, J., Ölveczky, P.C.: Formalization and correctness of the PALS architectural pattern for distributed real-time systems. Theoret. Comput. Sci. 451, 1–37 (2012)MathSciNetCrossRef

53.

Meseguer, J., Roşu, G.: The rewriting logic semantics project: a progress report. Inf. Comput. 231, 38–69 (2013)MathSciNetCrossRef

54.

Miller, S., Cofer, D., Sha, L., Meseguer, J., Al-Nayeem, A.: Implementing logical synchrony in integrated modular avionics. In: Proceedings of IEEE/AIAA 28th Digital Avionics Systems Conference. IEEE, USA (2009)

55.

Ölveczky, P.C., Boronat, A., Meseguer, J.: Formal semantics and analysis of behavioral AADL models in Real-Time Maude. In: Hatcliff, J., Zucca, E. (eds.) FMOODS/FORTE -2010. LNCS, vol. 6117, pp. 47–62. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-13464-7_5CrossRef

56.

Ölveczky, P.C., Boronat, A., Meseguer, J., Pek, E.: Formal semantics and analysis of behavioral AADL models in Real-Time Maude. https://olveczky.se/RealTimeMaude/AADL/webTechRep.pdf (2010)

57.

Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. High.-Order Symbolic Compu. 20(1–2), 161–196 (2007)CrossRef

58.

Ölveczky, P.C., Meseguer, J.: The Real-Time Maude Tool. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 332–336. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_23CrossRef

59.

Ölveczky, P.C.: Real-Time Maude and its applications. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 42–79. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12904-4_3CrossRef

60.

Ölveczky, P.C., Thorvaldsen, S.: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude. Theor. Comput. Sci. 410(2–3), 254–280 (2009). https://doi.org/10.1016/j.tcs.2008.09.022MathSciNetCrossRef

61.

Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143–189 (2008)MathSciNetCrossRef

62.

Ptolemaeus, C. (ed.): System Design, Modeling, and Simulation using Ptolemy II. Ptolemy.org (2014). http://ptolemy.org/books/Systems

63.

Rocha, C., Meseguer, J., Muñoz, C.: Rewriting modulo SMT and open system analysis. J. Logical Algebraic Methods Program. 86(1), 269–297 (2017)MathSciNetCrossRef

64.

Rubio, R., Martí-Oliet, N., Pita, I., Verdejo, A.: QMaude: quantitative specification and verification in rewriting logic. In: Chechik, M., Katoen, JP., Leucker, M. (eds.) Formal Methods. FM 2023. LNCS, vol. 14000. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-27481-7_15

65.

Rushby, J.: Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Trans. Software Eng. 25(5), 651–660 (1999)CrossRef

66.

Sha, L., Al-Nayeem, A., Sun, M., Meseguer, J., Ölveczky, P.C.: PALS: Physically asynchronous logically synchronous systems. Tech. rep., Department of Computer Science, University of Illinois at Urbana-Champaign (2009). http://hdl.handle.net/2142/11897

67.

Steiner, W., Bauer, G., Hall, B., Paulitsch, M., Varadarajan, S.: TTEthernet dataflow concept. In: 2009 Eighth IEEE International Symposium on Network Computing and Applications, pp. 319–322. IEEE (2009)

68.

Steiner, W., Rushby, J.: TTA and PALS: Formally verified design patterns for distributed cyber-physical systems. In: 2011 IEEE/AIAA 30th Digital Avionics Systems Conference, pp. 7B5–1. IEEE (2011)

69.

Stevens, B.L., Lewis, F.L.: Aircraft Control and Simulation. John Wiley & Sons (2003)

70.

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

71.

Whitters, G., Nigam, V., Talcott, C.L.: Incremental rewriting modulo SMT. In: Pientka, B., Tinelli, C. (eds.) Automated Deduction – CADE 29. CADE 2023. LNCS, vol. 14132. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-38499-8_32

72.

Yu, G., Bae, K.: Maude-SE: A tight integration of Maude and SMT solvers. Proc, International Workshop on Rewriting Logic and its Applications (2020)

73.

Yu, G., Lee, J., Bae, K.: STLMC: robust STL model checking of hybrid systems using SMT. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification. CAV 2022. LNCS, vol. 13371. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-13185-1_26

Title: Formal Model Engineering of Distributed CPSs Using AADL: From Behavioral AADL Models to Multirate Hybrid Synchronous AADL
Authors: Kyungmin Bae
Peter Csaba Ölveczky
Publisher: Springer Nature Switzerland
Book: Formal Aspects of Component Software
Print ISBN: 978-3-031-52182-9

Electronic ISBN: 978-3-031-52183-6

Copyright Year: 2024
DOI: https://doi.org/10.1007/978-3-031-52183-6_7

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner