nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

MARTE/pCCSL: Modeling and Refining Stochastic Behaviors of CPSs with Probabilistic Logical Clocks

verfasst von : Dehui Du, Ping Huang, Kaiqiang Jiang, Frédéric Mallet, Mingrui Yang

Erschienen in: Formal Aspects of Component Software

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Cyber-Physical Systems (CPSs) are networks of heterogeneous embedded systems immersed within a physical environment. Several ad-hoc frameworks and mathematical models have been studied to deal with challenging issues raised by CPSs. In this paper, we explore a more standard-based approach that relies on SysML/MARTE to capture different aspects of CPSs, including structure, behaviors, clock constraints, and non-functional properties. The novelty of our work lies in the use of logical clocks and MARTE/CCSL to drive and coordinate different models. Meanwhile, to capture stochastic behaviors of CPSs, we propose an extension of CCSL, called pCCSL, where logical clocks are adorned with stochastic properties. Possible variants are explored using Statistical Model Checking (SMC) via a transformation from the MARTE/pCCSL models into Stochastic Hybrid Automata. The whole process is illustrated through a case study of energy-aware building, in which the system is modeled by SysML/MARTE/pCCSL and different variants are explored through SMC to help expose the best alternative solutions.

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Constrained Synthesis from Component Libraries

Nächstes Kapitel A Formal and Run-Time Framework for the Adaptation of Local Behaviours to Match a Global Property

André, C.: Syntax and semantics of the Clock Constraint Specification Language (CCSL). Research Report 6925, INRIA, May 2009. http://hal.inria.fr/inria-00384077/

Arnold, A., Point, G., Griffault, A., Rauzy, A.: The altarica formalism for describing concurrent systems. Fundam. Inform. 40(2–3), 109–124 (1999)MathSciNetMATH

Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Le Guernic, P., de Simone, R.: The synchronous languages 12 years later. Proc. IEEE 91(1), 64–83 (2003)CrossRef

Berardinelli, L., Bernardi, S., Cortellessa, V., Merseguer, J.: UML profiles for non-functional properties at work: analyzing reliability, availability and performance. In: 2nd International Workshop on Non-functional System Properties in Domain Specific Modeling Languages (MoDELS/NFPinDSML), CEUR Workshop Proceedings, vol. 553. CEUR-WS.org (2009). http://ceur-ws.org/Vol-553/paper3.pdf

Bernardi, S., Merseguer, J., Petriu, D.C.: A dependability profile within MARTE. Softw. Syst. Model. 10(3), 313–336 (2011). http://dx.doi.org/10.1007/s10270-009-0128-1 CrossRef

Bohlender, D., Bruintjes, H., Junges, S., Katelaan, J., Nguyen, V.Y., Noll, T.: A review of statistical model checking pitfalls on real-time stochastic models. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 177–192. Springer, Heidelberg (2014). doi:10.1007/978-3-662-45231-8_13

Boudjadar, A.J., David, A., Kim, J.H., Larsen, K.G., Mikucionis, M., Nyman, U., Skou, A.: Schedulability and energy efficiency for multi-core hierarchical scheduling systems. In: ERTS (2014). http://www.erts2014.org/Site/0R4UXE94/Fichier/erts2014_1A1.pdf

Boutekkouk, F., Benmohammed, M., Bilavarn, S., Auguin, M.: UML2.0 profiles for embedded systems and systems on a chip (SOCs). J. Object Technol. 8(1), 135–157 (2009)CrossRef

Brosig, F., Meier, P., Becker, S., Koziolek, A., Koziolek, H., Kounev, S.: Quantitative evaluation of model-driven performance analysis and simulation of component-based architectures. IEEE Trans. Softw. Eng. 41(2), 157–175 (2015). http://dx.doi.org/10.1109/TSE.2014.2362755 CrossRef

10.

Bulychev, P., David, A., Larsen, K.G., Mikučionis, M., Poulsen, D.B., Legay, A., Wang, Z.: UPPAAL-SMC: statistical model checking for priced timed automata. arXiv preprint arXiv:1207.1272 (2012)

11.

David, A., Du, D., Larsen, K.G., Mikučionis, M., Skou, A.: An evaluation framework for energy aware buildings using statistical model checking. Sci. China Inf. Sci. 55(12), 2694–2707 (2012)CrossRef

12.

David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checker for biological systems. Int. J. Softw. Tools Technol. Transf. 17, 351–367 (2014)CrossRef

13.

David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., Vliet, J., Wang, Z.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80–96. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24310-3_7 CrossRef

14.

David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349–355. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_27 CrossRef

15.

DeAntoni, J., Mallet, F.: TimeSquare: treat your models with logical time. In: Furia, C.A., Nanz, S. (eds.) TOOLS 2012. LNCS, vol. 7304, pp. 34–41. Springer, Heidelberg (2012). doi:10.1007/978-3-642-30561-0_4 CrossRef

16.

Demathieu, S., Thomas, F., André, C., Gérard, S., Terrier, F.: First experiments using the UML profile for MARTE. In: 11th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC), pp. 50–57. IEEE (2008). http://dx.doi.org/10.1109/ISORC.2008.36

17.

Deshpande, A., Godbole, D., Göllü, A., Varaiya, P.: Design and evaluation tools for automated highway systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 138–148. Springer, Heidelberg (1996). doi:10.1007/BFb0020941 CrossRef

18.

Espinoza, H., Dubois, H., Gérard, S., Medina, J., Petriu, D.C., Woodside, M.: Annotating UML models with non-functional properties for quantitative analysis. In: Bruel, J.-M. (ed.) MODELS 2005. LNCS, vol. 3844, pp. 79–90. Springer, Heidelberg (2006). doi:10.1007/11663430_9 CrossRef

19.

Fang, H., Shi, J., Zhu, H., Guo, J., Larsen, K.G., David, A.: Formal verification and simulation for platform screen doors and collision avoidance in subway control systems. STTT 16(4), 339–361 (2014)CrossRef

20.

Fehnker, A., Ivančić, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326–341. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24743-2_22 CrossRef

21.

Iqbal, M.Z., Ali, S., Yue, T., Briand, L.: Experiences of applying UML/MARTE on three industrial projects. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds.) MODELS 2012. LNCS, vol. 7590, pp. 642–658. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33666-9_41 CrossRef

22.

Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and verification of a dual chamber implantable pacemaker. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 188–203. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28756-5_14 CrossRef

23.

Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)CrossRefMATH

24.

Lee, E.A., Sangiovanni-Vincentelli, A.L.: A framework for comparing models of computation. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 17(12), 1217–1229 (1998)CrossRef

25.

Lee, E.A.: Cyber physical systems: design challenges. In: 11th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC 2008), pp. 363–369. IEEE Computer Society, May 2008. http://dx.doi.org/10.1109/ISORC.2008.25

26.

Lee, E.A.: The past, present and future of cyber-physical systems: a focus on models. Sensors 15(3), 4837–4869 (2015). http://www.mdpi.com/1424-8220/15/3/4837 CrossRef

27.

Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16612-9_11 CrossRef

28.

Liu, J., Liu, Z., He, J., Mallet, F., Ding, Z.: Hybrid MARTE statecharts. Front. Comput. Sci. 7(1), 95–108 (2013)MathSciNetCrossRef

29.

Liu, Z., Liu, J., He, J., Ding, Z.: Spatio-temporal UML statechart for cyber-physical systems. In: 17th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS, pp. 137–146. IEEE Computer Society (2012). http://doi.ieeecomputersociety.org/10.1109/ICECCS.2012.36

30.

Mallet, F., de Simone, R.: Correctness issues on MARTE/CCSL constraints. Sci. Comput. Program. 106, 78–92 (2015). http://www.sciencedirect.com/science/article/pii/S0167642315000519 CrossRef

31.

Ptolemaeus, C.: System Design, Modeling, and Simulation: Using Ptolemy II. Ptolemy.org, New York (2014)

32.

Selic, B., Gerard, S.: Modeling and Analysis of Real-Time and Embedded Systems with UML and MARTE. Elsevier, Amsterdam (2013)

33.

Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004). doi:10.1007/978-3-540-27813-9_16 CrossRef

34.

Shorin, D., Zimmermann, A., Maciel, P.: Transforming UML state machines into stochastic petri nets for energy consumption estimation of embedded systems. Sustain. Internet ICT Sustain. (SustainIT) 2012, 1–6 (2012)

35.

Shorin, D., Zimmermann, A.: Formal description of an approach for power consumption estimation of embedded systems. In: 24th International Workshop on Power and Timing Modeling, Optimization and Simulation, PATMOS, pp. 1–10 (2014). http://dx.doi.org/10.1109/PATMOS.2014.6951890

36.

Suryadevara, J., Seceleanu, C., Mallet, F., Pettersson, P.: Verifying MARTE/CCSL mode behaviors using UPPAAL. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 1–15. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40561-7_1 CrossRef

37.

Tomlin, C., Pappas, G., Lygeros, J., Godbole, D., Sastry, S.: Hybrid control models of next generation air traffic management. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1996. LNCS, vol. 1273, pp. 378–404. Springer, Heidelberg (1997). doi:10.1007/BFb0031570 CrossRef

38.

Tribastone, M., Gilmore, S.: Automatic extraction of PEPA performance models from UML activity diagrams annotated with the MARTE profile. In: Avritzer, A., Weyuker, E.J., Woodside, C.M. (eds.) 7th International Workshop on Software and Performance, WOSP 2008, pp. 67–78. ACM (2008). http://doi.acm.org/10.1145/1383559.1383569

39.

Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput. 204(9), 1368–1409 (2006). http://dx.doi.org/10.1016/j.ic.2006.05.002 MathSciNetCrossRefMATH

40.

Zhang, Y., Mallet, F., Chen, Y.: Timed automata semantics of spatial-temporal consistency language STeC. In: Theoretical Aspects of Software Engineering Conference, TASE, pp. 201–208. IEEE (2014). http://dx.doi.org/10.1109/TASE.2014.10

41.

Zou, J., Matic, S., Lee, E.A., Feng, T.H., Derler, P.: Execution strategies for PTIDES, a programming model for distributed embedded systems. In: 15th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS, pp. 77–86. IEEE Computer Society (2009). http://dx.doi.org/10.1109/RTAS.2009.39

Titel: MARTE/pCCSL: Modeling and Refining Stochastic Behaviors of CPSs with Probabilistic Logical Clocks
verfasst von: Dehui Du
Ping Huang
Kaiqiang Jiang
Frédéric Mallet
Mingrui Yang
Verlag: Springer International Publishing
Buch: Formal Aspects of Component Software
Print ISBN: 978-3-319-57665-7

Electronic ISBN: 978-3-319-57666-4

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-57666-4_8

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"