Abstract
SysML activity diagram is a standard modeling language for complex systems. It supports systems’ composition by providing the operator ‘call behavior’. In general, the verification of systems modeled with those diagram inherit the limitations of the developed built-in tools, especially the case of model checking. To address this shortcoming, we propose a compositional verification framework based on the call behavior operator to alleviate the state space explosion problem of model-checking. The framework decomposes a property into local sub-properties and verify them separately on the composed behavioral diagrams. Further, we propose to ignore the diagrams’ artifacts that are useless with respect to the property under verification. We prove the soundness of the proposed approach by showing that the result deduced from the verification of the local properties is always preserved. The verification results are obtained by encoding SysML activity diagrams in the probabilistic model checker ‘PRISM’. Finally, we demonstrate the effectiveness of our framework by verifying a set of properties on two use cases that require a large amount of memory and a considerable time processing.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
http://www.prismmodelchecker.org/doc/manual.pdf (The introduction section, line 10).
- 3.
The model size is the number of transitions (edges).
- 4.
Each call-behavior action is represented by its proper diagram.
- 5.
The call behavior action “Check Card” is denoted by \(a'\) and calls the diagram \(\mathscr {A}'_1\).
References
Ando, T., Yatsu, H., Kong, W., Hisazumi, K., Fukuda, A.: Formalization and model checking of SysML state machine diagrams by CSP#. In: Murgante, B., et al. (eds.) ICCSA 2013. LNCS, vol. 7973, pp. 114–127. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39646-5_9
Andrade, E., Maciel, P., Callou, G., Nogueira, B.: A methodology for mapping SysML activity diagram to time petri net for requirement validation of embedded real-time systems with energy constraints. In: ICDS 2009: Proceedings of the 2009 Third International Conference on Diagrams Society, pp. 266–271. IEEE Computer Society, Washington, DC (2009)
Apvrille, L., de Saqui-Sannes, P.: Static analysis techniques to verify mutual exclusion situations within SysML models. In: Khendek, F., Toeroe, M., Gherbi, A., Reed, R. (eds.) SDL 2013. LNCS, vol. 7916, pp. 91–106. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38911-5_6
Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)
Bérard, B.: Systems and Software Verification. Springer, Heidelberg (2001). https://doi.org/10.1007/978-3-662-04558-9
Berezin, S., Campos, S., Clarke, E.M.: Compositional reasoning in model checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 81–102. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-49213-5_4
Carneiro, E., Maciel, P., Callou, G., Tavares, E., Nogueira, B.: Mapping SysML state machine diagram to time petri net for analysis and verification of embedded real-time systems with energy constraints. In: ENICS 2008: Proceedings of the 2008 International Conference on Advances in Electronics and Micro-electronics, pp. 1–6. IEEE Computer Society, Washington, DC (2008)
Carrillo, O., Chouali, S., Mountassir, H.: Formalizing and verifying compatibility and consistency of SYSML blocks. SIGSOFT Softw. Eng. Notes 37(4), 1–8 (2012)
Feng, L., Han, T., Kwiatkowska, M., Parker, D.: Learning-based compositional verification for synchronous probabilistic systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 511–521. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24372-1_40
Feng, L., Kwiatkowska, M., Parker, D.: Compositional verification of probabilistic systems using learning. In: Proceedings of the 2010 Seventh International Conference on the Quantitative Evaluation of Systems, QEST 2010, pp. 133–142. IEEE Computer Society (2010)
Feng, L., Kwiatkowska, M., Parker, D.: Automated learning of probabilistic assumptions for compositional reasoning. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 2–17. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19811-3_2
Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21455-4_3
Gomaa, H.: Software Modeling and Design: UML, Use Cases, Patterns, and Software Architectures. Cambridge University Press, Cambridge (2011)
Object Management Group. OMG Unified Modeling Language: Superstructure 2.1.2, November 2007
Holt, J., Perry, J.: SysML for Systems Engineering. Institution of Engineering and Technology Press, January 2007
Huang, X., Sun, Q., Li, J., Zhang, T.: MDE-based verification of SysML state machine diagram by UPPAAL. In: Yuyu Yuan, X.W., Yueming, L. (eds.) Trustworthy Computing and Services. CCIS, vol. 320, pp. 490–497. Springer, Berlin Heidelberg (2013)
Jansen, D.N., Hermanns, H., Katoen, J.-P.: A probabilistic extension of UML statecharts. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 355–374. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45739-9_21
Jansen, D.N., Hermanns, H., Katoen, J.-P.: A QoS-oriented extension of UML statecharts. In: Stevens, P., Whittle, J., Booch, G. (eds.) UML 2003. LNCS, vol. 2863, pp. 76–91. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45221-8_7
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47
Object Management Group. OMG Systems Modeling Language Specification, September 2007
Ouchani, S., Mohamed, O.A., Debbabi, M.: A security risk assessment framework for SYSML activity diagrams. In: 2013 IEEE 7th International Conference on Software Security and Reliability, pp. 227–236, June 2013
Ouchani, S.: Towards a fractionation-based verification: application on SYSML activity diagrams. In: Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing, SAC 2019, pp. 2032–2039. ACM (2019)
Ouchani, S., Debbabi, M.: Specification, verification, and quantification of security in model-based systems. Computing 97(7), 691–711 (2015)
Ouchani, S., Ait Mohamed, O., Debbabi, M.: Efficient probabilistic abstraction for SysML activity diagrams. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 263–277. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33826-7_18
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Ouchani, S. (2019). Towards a Call Behavior-Based Compositional Verification Framework for SysML Activity Diagrams. In: Hierons, R., Mosbah, M. (eds) Theoretical Aspects of Computing – ICTAC 2019. ICTAC 2019. Lecture Notes in Computer Science(), vol 11884. Springer, Cham. https://doi.org/10.1007/978-3-030-32505-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-030-32505-3_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-32504-6
Online ISBN: 978-3-030-32505-3
eBook Packages: Computer ScienceComputer Science (R0)