Advertisement

Towards a Call Behavior-Based Compositional Verification Framework for SysML Activity Diagrams

  • Samir OuchaniEmail author
Conference paper
First Online:
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11884)

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.

Keywords

SysML Activity diagrams Model-checking Compositional verification Abstraction PCTL PRISM 
This is a preview of subscription content, log in to check access.

References

  1. 1.
    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_9CrossRefGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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_6CrossRefGoogle Scholar
  4. 4.
    Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  5. 5.
    Bérard, B.: Systems and Software Verification. Springer, Heidelberg (2001).  https://doi.org/10.1007/978-3-662-04558-9CrossRefGoogle Scholar
  6. 6.
    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_4CrossRefGoogle Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    Carrillo, O., Chouali, S., Mountassir, H.: Formalizing and verifying compatibility and consistency of SYSML blocks. SIGSOFT Softw. Eng. Notes 37(4), 1–8 (2012)CrossRefGoogle Scholar
  9. 9.
    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_40CrossRefzbMATHGoogle Scholar
  10. 10.
    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)Google Scholar
  11. 11.
    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_2CrossRefGoogle Scholar
  12. 12.
    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_3CrossRefGoogle Scholar
  13. 13.
    Gomaa, H.: Software Modeling and Design: UML, Use Cases, Patterns, and Software Architectures. Cambridge University Press, Cambridge (2011)CrossRefGoogle Scholar
  14. 14.
    Object Management Group. OMG Unified Modeling Language: Superstructure 2.1.2, November 2007Google Scholar
  15. 15.
    Holt, J., Perry, J.: SysML for Systems Engineering. Institution of Engineering and Technology Press, January 2007Google Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    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_21CrossRefzbMATHGoogle Scholar
  18. 18.
    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_7CrossRefGoogle Scholar
  19. 19.
    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_47CrossRefGoogle Scholar
  20. 20.
    Object Management Group. OMG Systems Modeling Language Specification, September 2007Google Scholar
  21. 21.
    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 2013Google Scholar
  22. 22.
    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)Google Scholar
  23. 23.
    Ouchani, S., Debbabi, M.: Specification, verification, and quantification of security in model-based systems. Computing 97(7), 691–711 (2015)MathSciNetCrossRefGoogle Scholar
  24. 24.
    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_18CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.LINEACT, Laboratoire d’Innovation Numérique École d’Ingénieur CESIAix-en-ProvenceFrance

Personalised recommendations

Cite paper

Buy options