Skip to main content
Erschienen in:

03.09.2022 | General

Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL

verfasst von: Jaehun Lee, Kyungmin Bae, Peter Csaba Ölveczky, Sharon Kim, Minseok Kang

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 6/2022

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

This paper presents the HybridSynchAADL modeling language and formal analysis tool for virtually synchronous cyber-physical systems with complex control programs, continuous behaviors, and bounded clock skews, network delays, and execution times. We leverage the Hybrid PALS methodology, so that it is sufficient to model and verify the much simpler underlying synchronous designs. We define the HybridSynchAADL language as a sublanguage of the avionics modeling standard AADL for modeling such synchronous designs in AADL. We define the formal semantics of HybridSynchAADL using Maude with SMT solving, which allows us to represent advanced control programs and communication features in Maude, while capturing timing uncertainties and continuous behaviors symbolically with SMT solving. We have developed new general methods for optimizing the performance of such symbolic rewriting, which makes the analysis of HybridSynchAADL models feasible. We have integrated the formal modeling and analysis of HybridSynchAADL models into the OSATE tool environment for AADL. Finally, we demonstrate the effectiveness of the Hybrid PALS methodology and HybridSynchAADL on a number of applications, including autonomous drones that collaborate to achieve common goals, and compare the performance of our tool with other state-of-the-art formal tools for hybrid systems.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

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!

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!

Fußnoten
1
If, in addition, all message delays are 0, then the asynchronous system has more than 3 million reachable states, and its model checking takes more than 30 minutes.
 
2
Although we present HybridSynchAADL in the context of Hybrid PALS, our language and tool can more generally be used to model and formally analyze any “synchronous” CPSs with continuous local environments that are sampled/actuated based on imprecise local clocks.
 
3
Given performance bounds \(\Gamma \), PALS can find the shortest period p that allows all nodes to read the messages in the correct “rounds.”
 
5
Hardware components include: processor components that schedule and execute threads, memory components, device components, and bus components that interconnect processors, memory, and devices.
 
6
A rewrite condition \(t_j \longrightarrow t_j'\) holds if (a substitution instance of) \(t_j'\) is reachable from (the substitution instance of) \(t_j\) in zero or more steps.
 
7
There exist specialized solvers to support SMT solving with ODEs [35]. Because they have not been integrated with Maude, the current version only supports continuous functions.
 
8
A component path is given by a period-separated path of component identifiers in AADL; for example,
 
9
Since the period of the system is 10 (ms), we search for states reachable within \(30/10=3\) iterations/steps of the system.
 
10
We have developed a variety of HybridSynchAADL models for rendezvous and formation control of different numbers of drones with single-integrator and double-integrator dynamics. All of them are available at https://​hybridsynchaadl.​github.​io.
 
11
We use equivalent control logic for both HybridSynchAADL models and hybrid automata models. For the drone rendezvous models, the control logics used in this experiment are simplified from one presented in Sect. 8.
 
Literatur
1.
Zurück zum Zitat Steiner, W., Bauer, G., Hall, B., Paulitsch, M., Varadarajan, S.: TTEthernet dataflow concept. In: IEEE International Symposium on Network Computing and Applications, pp. 319–322 (2009). IEEE Steiner, W., Bauer, G., Hall, B., Paulitsch, M., Varadarajan, S.: TTEthernet dataflow concept. In: IEEE International Symposium on Network Computing and Applications, pp. 319–322 (2009). IEEE
2.
Zurück zum Zitat Leen, G., Heffernan, D., Dunne, A.: Digital networks in the automotive vehicle. Comput. Control Eng. J. 10(6), 257–266 (1999)CrossRef Leen, G., Heffernan, D., Dunne, A.: Digital networks in the automotive vehicle. Comput. Control Eng. J. 10(6), 257–266 (1999)CrossRef
3.
Zurück zum Zitat 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 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
4.
Zurück zum Zitat 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 (2007). IEEE 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 (2007). IEEE
5.
Zurück zum Zitat 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: Proceedings of ICCPS, pp. 149–158 (2010) 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: Proceedings of ICCPS, pp. 149–158 (2010)
6.
Zurück zum Zitat Abrial, J., Börger, E., Langmaack, H. (eds.): Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, vol. 1165. LNCS, Springer, Berlin (1996)MATH Abrial, J., Börger, E., Langmaack, H. (eds.): Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, vol. 1165. LNCS, Springer, Berlin (1996)MATH
7.
Zurück zum Zitat 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) 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)
8.
Zurück zum Zitat 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) 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)
9.
Zurück zum Zitat Meseguer, J., Ölveczky, P.C.: Formalization and correctness of the PALS architectural pattern for distributed real-time systems. Theor. Comput. Sci. 451, 1–37 (2012)MathSciNetCrossRefMATH Meseguer, J., Ölveczky, P.C.: Formalization and correctness of the PALS architectural pattern for distributed real-time systems. Theor. Comput. Sci. 451, 1–37 (2012)MathSciNetCrossRefMATH
10.
Zurück zum Zitat 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) 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)
11.
Zurück zum Zitat Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis and Design Language. Addison-Wesley (2012) Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis and Design Language. Addison-Wesley (2012)
12.
Zurück zum Zitat França, R.B., Bodeveix, J.-P., Filali, M., Rolland, J.-F., Chemouil, D., Thomas, D.: The AADL Behaviour Annex—experiments and roadmap. In: Proceedings of ICECCS. IEEE (2007) França, R.B., Bodeveix, J.-P., Filali, M., Rolland, J.-F., Chemouil, D., Thomas, D.: The AADL Behaviour Annex—experiments and roadmap. In: Proceedings of ICECCS. IEEE (2007)
13.
Zurück zum Zitat Clavel, M., Durán, F., Eker, S., Meseguer, J., Lincoln, P., Martí-Oliet, N., Talcott, C.: All About Maude—A High-Performance Logical Framework, vol. 4350. LNCS, Springer, Berlin (2007)MATH Clavel, M., Durán, F., Eker, S., Meseguer, J., Lincoln, P., Martí-Oliet, N., Talcott, C.: All About Maude—A High-Performance Logical Framework, vol. 4350. LNCS, Springer, Berlin (2007)MATH
14.
Zurück zum Zitat Rocha, C., Meseguer, J., Muñoz, C.: Rewriting modulo SMT and open system analysis. J. Log. Algebraic Methods Program. 86(1), 269–297 (2017)MathSciNetCrossRefMATH Rocha, C., Meseguer, J., Muñoz, C.: Rewriting modulo SMT and open system analysis. J. Log. Algebraic Methods Program. 86(1), 269–297 (2017)MathSciNetCrossRefMATH
15.
Zurück zum Zitat Bae, K., Rocha, C.: Symbolic state space reduction with guarded terms for rewriting modulo SMT. Sci. Comput. Program. 178, 20–42 (2019)CrossRef Bae, K., Rocha, C.: Symbolic state space reduction with guarded terms for rewriting modulo SMT. Sci. Comput. Program. 178, 20–42 (2019)CrossRef
16.
Zurück zum Zitat Baldoni, R., Coppa, E., D’Elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. (CSUR) 51(3), 1–39 (2018)CrossRef Baldoni, R., Coppa, E., D’Elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. (CSUR) 51(3), 1–39 (2018)CrossRef
17.
Zurück zum Zitat Dutertre, B.: Yices 2.2. In: Proceedings of CAV. LNCS, vol. 8559, pp. 737–744. Springer, Berlin (2014) Dutertre, B.: Yices 2.2. In: Proceedings of CAV. LNCS, vol. 8559, pp. 737–744. Springer, Berlin (2014)
18.
Zurück zum Zitat Lee, J., Kim, S., Bae, K., Ölveczky, P.C.: HybridSynchAADL: modeling and formal analysis of virtually synchronous CPSs in AADL. In: Proceedings of CAV’21. LNCS, vol. 12759, pp. 491–504. Springer, Berlin (2021) Lee, J., Kim, S., Bae, K., Ölveczky, P.C.: HybridSynchAADL: modeling and formal analysis of virtually synchronous CPSs in AADL. In: Proceedings of CAV’21. LNCS, vol. 12759, pp. 491–504. Springer, Berlin (2021)
19.
Zurück zum Zitat Rushby, J.: Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Trans. Softw. Eng. 25(5), 651–660 (1999)CrossRef Rushby, J.: Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Trans. Softw. Eng. 25(5), 651–660 (1999)CrossRef
20.
Zurück zum Zitat Bae, K., Ölveczky, P.C.: MSYNC: a generalized formal design pattern for virtually synchronous multirate cyber-physical systems. In: ACM Transactions on Embedded Computing Systems (Proceedings of EMSOFT’21), vol. 20, no. 5s, Article 105 (2021) Bae, K., Ölveczky, P.C.: MSYNC: a generalized formal design pattern for virtually synchronous multirate cyber-physical systems. In: ACM Transactions on Embedded Computing Systems (Proceedings of EMSOFT’21), vol. 20, no. 5s, Article 105 (2021)
21.
Zurück zum Zitat Caspi, P., Mazuet, C., Paligot, N.R.: About the design of distributed control systems: the quasi-synchronous approach. In: International Conference on Computer Safety, Reliability, and Security (2001). Springer Caspi, P., Mazuet, C., Paligot, N.R.: About the design of distributed control systems: the quasi-synchronous approach. In: International Conference on Computer Safety, Reliability, and Security (2001). Springer
22.
Zurück zum Zitat 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)MathSciNetCrossRefMATH 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)MathSciNetCrossRefMATH
23.
Zurück zum Zitat Bae, K., Meseguer, J., Ölveczky, P.C.: Formal patterns for multirate distributed real-time systems. Sci. Comput. Program. 91, 3–44 (2014)CrossRef Bae, K., Meseguer, J., Ölveczky, P.C.: Formal patterns for multirate distributed real-time systems. Sci. Comput. Program. 91, 3–44 (2014)CrossRef
24.
Zurück zum Zitat 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. 7–51 (2011). IEEE 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. 7–51 (2011). IEEE
25.
Zurück zum Zitat Skeirik, S., Stefanescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. Fund. Inform. 173(4), 315–382 (2020)MathSciNetMATH Skeirik, S., Stefanescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. Fund. Inform. 173(4), 315–382 (2020)MathSciNetMATH
27.
28.
Zurück zum Zitat Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV, pp. 171–177 (2011). Springer Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV, pp. 171–177 (2011). Springer
29.
Zurück zum Zitat Barrett, C., Stump, A., Tinelli, C., et al.: The SMT-LIB standard: version 2.0. In: SMT, vol. 13, p. 14 (2010) Barrett, C., Stump, A., Tinelli, C., et al.: The SMT-LIB standard: version 2.0. In: SMT, vol. 13, p. 14 (2010)
30.
Zurück zum Zitat Ahmad, E., Larson, B.R., Barrett, S.C., Zhan, N., Dong, Y.: Hybrid Annex: an AADL extension for continuous behavior and cyber-physical interaction modeling. In: Proceedings of ACM SIGAda Annual Conference on High Integrity Language Technology (HILT’14). ACM, New York (2014) Ahmad, E., Larson, B.R., Barrett, S.C., Zhan, N., Dong, Y.: Hybrid Annex: an AADL extension for continuous behavior and cyber-physical interaction modeling. In: Proceedings of ACM SIGAda Annual Conference on High Integrity Language Technology (HILT’14). ACM, New York (2014)
31.
Zurück zum Zitat Qian, Y., Liu, J., Chen, X.: Hybrid AADL: a sublanguage extension to AADL. In: Proceedings of Internetware’13. ACM, New York (2013) Qian, Y., Liu, J., Chen, X.: Hybrid AADL: a sublanguage extension to AADL. In: Proceedings of Internetware’13. ACM, New York (2013)
32.
Zurück zum Zitat Bae, K., Ölveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of multirate synchronous AADL. In: Proceedings of FM’14. LNCS, vol. 8442. Springer, Berlin (2014) Bae, K., Ölveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of multirate synchronous AADL. In: Proceedings of FM’14. LNCS, vol. 8442. Springer, Berlin (2014)
33.
Zurück zum Zitat Bae, K., Ölveczky, P.C., Al-Nayeem, A., Meseguer, J.: Synchronous AADL and its formal analysis in Real-Time Maude. In: Proceedings of ICFEM’11, vol. 6991. LNCS, Springer, Berlin (2011) Bae, K., Ölveczky, P.C., Al-Nayeem, A., Meseguer, J.: Synchronous AADL and its formal analysis in Real-Time Maude. In: Proceedings of ICFEM’11, vol. 6991. LNCS, Springer, Berlin (2011)
34.
Zurück zum Zitat Ölveczky, P.C., Boronat, A., Meseguer, J.: Formal semantics and analysis of behavioral AADL models in Real-Time Maude. In: Formal Techniques for Distributed Systems, pp. 47–62. Springer, Berlin (2010) Ölveczky, P.C., Boronat, A., Meseguer, J.: Formal semantics and analysis of behavioral AADL models in Real-Time Maude. In: Formal Techniques for Distributed Systems, pp. 47–62. Springer, Berlin (2010)
35.
Zurück zum Zitat Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Proceedings of CADE, vol. 7898, pp. 208–214. LNCS, Springer, Berlin (2013) Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Proceedings of CADE, vol. 7898, pp. 208–214. LNCS, Springer, Berlin (2013)
36.
Zurück zum Zitat Ren, W., Beard, R.W.: Distributed Consensus in Multi-vehicle Cooperative Control. Springer, Berlin (2008)CrossRefMATH Ren, W., Beard, R.W.: Distributed Consensus in Multi-vehicle Cooperative Control. Springer, Berlin (2008)CrossRefMATH
37.
Zurück zum Zitat Henzinger, T.: The theory of hybrid automata. In: Verification of Digital and Hybrid Systems. NATO ASI Series, vol. 170, pp. 265–292. Springer, Berlin, Heidelberg (2000) Henzinger, T.: The theory of hybrid automata. In: Verification of Digital and Hybrid Systems. NATO ASI Series, vol. 170, pp. 265–292. Springer, Berlin, Heidelberg (2000)
38.
Zurück zum Zitat Bae, K., Gao, S.: Modular SMT-based analysis of nonlinear hybrid systems. In: Proceedings of FMCAD, pp. 180–187. IEEE (2017) Bae, K., Gao, S.: Modular SMT-based analysis of nonlinear hybrid systems. In: Proceedings of FMCAD, pp. 180–187. IEEE (2017)
39.
Zurück zum Zitat Raisch, J., Klein, E., Meder, C., Itigin, A., O’Young, S.: Approximating automata and discrete control for continuous systems—two examples from process control. In: Hybrid Systems V, pp. 279–303. Springer, Berlin (1999) Raisch, J., Klein, E., Meder, C., Itigin, A., O’Young, S.: Approximating automata and discrete control for continuous systems—two examples from process control. In: Hybrid Systems V, pp. 279–303. Springer, Berlin (1999)
40.
Zurück zum Zitat Yu, G., Bae, K.: Maude-SE: a tight integration of Maude and SMT solvers. In: Proceedings of International Workshop on Rewriting Logic and its Applications (2020) Yu, G., Bae, K.: Maude-SE: a tight integration of Maude and SMT solvers. In: Proceedings of International Workshop on Rewriting Logic and its Applications (2020)
41.
Zurück zum Zitat Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: Proceedings of TACAS, vol. 9035. LNCS, Springer, Berlin (2015) Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: Proceedings of TACAS, vol. 9035. LNCS, Springer, Berlin (2015)
42.
Zurück zum Zitat Frehse, G., Guernic, C.L., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Proceedings of CAV, vol. 6806. LNCS, Springer, Berlin (2011) Frehse, G., Guernic, C.L., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Proceedings of CAV, vol. 6806. LNCS, Springer, Berlin (2011)
43.
Zurück zum Zitat Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Proceedings of CAV, pp. 258–263 (2013). Springer Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Proceedings of CAV, pp. 258–263 (2013). Springer
44.
Zurück zum Zitat Kong, S., Gao, S., Chen, W., Clarke, E.M.: dReach: \(\delta \)-reachability analysis for hybrid systems. In: Proceedings of TACAS, vol. 7898, pp. 200–205. LNCS, Springer, Berlin (2015) Kong, S., Gao, S., Chen, W., Clarke, E.M.: dReach: \(\delta \)-reachability analysis for hybrid systems. In: Proceedings of TACAS, vol. 7898, pp. 200–205. LNCS, Springer, Berlin (2015)
45.
Zurück zum Zitat Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: Proceedings of HSCC’15, pp. 128–133 (2015) Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: Proceedings of HSCC’15, pp. 128–133 (2015)
46.
Zurück zum Zitat Ahmad, E., Dong, Y., Wang, S., Zhan, N., Zou, L.: Adding formal meanings to AADL with Hybrid Annex. In: Proceedings of FACS, vol. 8997. LNCS, Springer, Berlin (2015) Ahmad, E., Dong, Y., Wang, S., Zhan, N., Zou, L.: Adding formal meanings to AADL with Hybrid Annex. In: Proceedings of FACS, vol. 8997. LNCS, Springer, Berlin (2015)
47.
Zurück zum Zitat Bao, Y., Chen, M., Zhu, Q., Wei, T., Mallet, F., Zhou, T.: Quantitative performance evaluation of uncertainty-aware Hybrid AADL designs using statistical model checking. IEEE Trans. CAD Integr. Circuits Syst. 36(12), 1989–2002 (2017)CrossRef Bao, Y., Chen, M., Zhu, Q., Wei, T., Mallet, F., Zhou, T.: Quantitative performance evaluation of uncertainty-aware Hybrid AADL designs using statistical model checking. IEEE Trans. CAD Integr. Circuits Syst. 36(12), 1989–2002 (2017)CrossRef
48.
Zurück zum Zitat Liu, J., Li, T., Ding, Z., Qian, Y., Sun, H., He, J.: AADL+: a simulation-based methodology for cyber-physical systems. Front. Comput. Sci. 13(3), 516–538 (2019)CrossRef Liu, J., Li, T., Ding, Z., Qian, Y., Sun, H., He, J.: AADL+: a simulation-based methodology for cyber-physical systems. Front. Comput. Sci. 13(3), 516–538 (2019)CrossRef
49.
Zurück zum Zitat Bae, K., Ölveczky, P.C., Meseguer, J., Al-Nayeem, A.: The SynchAADL2Maude tool. In: Proceedings of FASE’12, vol. 7212. LNCS, Springer, Berlin (2012) Bae, K., Ölveczky, P.C., Meseguer, J., Al-Nayeem, A.: The SynchAADL2Maude tool. In: Proceedings of FASE’12, vol. 7212. LNCS, Springer, Berlin (2012)
50.
Zurück zum Zitat Baudart, G., Bourke, T., Pouzet, M.: Soundness of the quasi-synchronous abstraction. In: Proceedings of FMCAD, pp. 9–16 (2016). IEEE Baudart, G., Bourke, T., Pouzet, M.: Soundness of the quasi-synchronous abstraction. In: Proceedings of FMCAD, pp. 9–16 (2016). IEEE
51.
Zurück zum Zitat Larrieu, R., Shankar, N.: A framework for high-assurance quasi-synchronous systems. In: Proceedings of MEMOCODE, pp. 72–83 (2014). IEEE Larrieu, R., Shankar, N.: A framework for high-assurance quasi-synchronous systems. In: Proceedings of MEMOCODE, pp. 72–83 (2014). IEEE
52.
Zurück zum Zitat Halbwachs, N., Mandel, L.: Simulation and verification of asynchronous systems by means of a synchronous model. In: Sixth International Conference on Application of Concurrency to System Design (ACSD’06), pp. 3–14 (2006). IEEE Halbwachs, N., Mandel, L.: Simulation and verification of asynchronous systems by means of a synchronous model. In: Sixth International Conference on Application of Concurrency to System Design (ACSD’06), pp. 3–14 (2006). IEEE
53.
Zurück zum Zitat Girault, A., Ménier, C.: Automatic production of globally asynchronous locally synchronous systems. In: International Workshop on Embedded Software, pp. 266–281 (2002). Springer Girault, A., Ménier, C.: Automatic production of globally asynchronous locally synchronous systems. In: International Workshop on Embedded Software, pp. 266–281 (2002). Springer
54.
Zurück zum Zitat Potop-Butucaru, D., Caillaud, B.: Correct-by-construction asynchronous implementation of modular synchronous specifications. Fund. Inform. 78(1), 131–159 (2007)MathSciNetMATH Potop-Butucaru, D., Caillaud, B.: Correct-by-construction asynchronous implementation of modular synchronous specifications. Fund. Inform. 78(1), 131–159 (2007)MathSciNetMATH
55.
Zurück zum Zitat Desai, A., Seshia, S.A., Qadeer, S., Broman, D., Eidson, J.C.: Approximate synchrony: an abstraction for distributed almost-synchronous systems. In: Proceedings of CAV’15. LNCS, vol. 9207, pp. 429–448. Springer, Berlin (2015) Desai, A., Seshia, S.A., Qadeer, S., Broman, D., Eidson, J.C.: Approximate synchrony: an abstraction for distributed almost-synchronous systems. In: Proceedings of CAV’15. LNCS, vol. 9207, pp. 429–448. Springer, Berlin (2015)
56.
Zurück zum Zitat Bak, S., Duggirala, P.S.: Hylaa: a tool for computing simulation-equivalent reachability for linear systems. In: Proceedings of HSCC, pp. 173–178 (2017) Bak, S., Duggirala, P.S.: Hylaa: a tool for computing simulation-equivalent reachability for linear systems. In: Proceedings of HSCC, pp. 173–178 (2017)
57.
Zurück zum Zitat Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, vol. 3253, pp. 152–166. LNCS, Springer, Berlin (2004) Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, vol. 3253, pp. 152–166. LNCS, Springer, Berlin (2004)
58.
Zurück zum Zitat Bae, K., Lee, J.: Bounded model checking of signal temporal logic properties using syntactic separation. In: Proceedings of ACM Programming Language, vol. 3 (POPL) (Proceedings of POPL 2019) (2019) Bae, K., Lee, J.: Bounded model checking of signal temporal logic properties using syntactic separation. In: Proceedings of ACM Programming Language, vol. 3 (POPL) (Proceedings of POPL 2019) (2019)
59.
Zurück zum Zitat Lee, J., Yu, G., Bae, K.: Efficient SMT-based model checking for signal temporal logic. In: Proceedings of 36th IEEE/ACM International Conference on Automated Software Engineering (ASE’21), pp. 343–354 (2021). IEEE Lee, J., Yu, G., Bae, K.: Efficient SMT-based model checking for signal temporal logic. In: Proceedings of 36th IEEE/ACM International Conference on Automated Software Engineering (ASE’21), pp. 343–354 (2021). IEEE
60.
Zurück zum Zitat Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6–1639 (2018)MathSciNetCrossRef Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6–1639 (2018)MathSciNetCrossRef
61.
Zurück zum Zitat AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Proceedings of CALCO 2011, vol. 6859, pp. 386–392. LNCS, Springer, Berlin (2011) AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Proceedings of CALCO 2011, vol. 6859, pp. 386–392. LNCS, Springer, Berlin (2011)
62.
Zurück zum Zitat Agha, G.A., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electron. Notes Theor. Comput. Sci. 153(2), 213–239 (2006)CrossRef Agha, G.A., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electron. Notes Theor. Comput. Sci. 153(2), 213–239 (2006)CrossRef
Metadaten
Titel
Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL
verfasst von
Jaehun Lee
Kyungmin Bae
Peter Csaba Ölveczky
Sharon Kim
Minseok Kang
Publikationsdatum
03.09.2022
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 6/2022
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-022-00665-z

Weitere Artikel der Ausgabe 6/2022

International Journal on Software Tools for Technology Transfer 6/2022 Zur Ausgabe

Premium Partner