Abstract
During the process of utilizing Model-Based Systems Engineering (MBSE), SysML activity diagrams are often used for designing the software systems and its correctness is likely to significantly affect the reliability of the implementation. However, how to effectively verify the correctness of SysML diagrams still remains a challenge and to the best of our knowledge, there are few tools to support the verification of SysML models. Testing-based formal verification (TBFV) is designed for verifying the sequence code. To solve the problem, we creatively apply the existing TBFV approach into the verification of SysML activity diagrams and established a new approach, called TBFV-M. TBFV-M has ability to verify a SysML activity diagrams meet the user’ need. We also propose a method to dealing with invocation, because invocation is very common in the model-driven development process. In this paper, we describe the principle of TBFV-M and present a case study to demonstrate its feasibility and usability. Finally, we conclude the paper and point out future research directions.
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
References
Wymore, A.W.: Model-Based Systems Engineering: An Introduction to the Mathematical Theory of Discrete Systems and to the Tricotyledon Theory of System Design. CRC Press, Boca Raton (1993)
Friedenthal, S., Moore, A., Steiner, R.: A practical guide to sysml. San Francisco Jung Inst. Libr. J. 17(1), 41–46 (2012)
Weilkiens, T.: Systems engineering with SysML/UML. Computer (6), 83 (2006)
Shah, M., et al.: Knowledge engineering tools in planning: state-of-the-art and future challenges. Computer (2013)
Vaquero, T.S., Silva, J.R., Beck, C.J.: A brief review of tools and methods for knowledge engineering for planning scheduling. Computer 7–14 (2011)
Liu, S.: Utilizing hoare logic to strengthen testing for error detection in programs. Computer 50(6), 1–5 (2014)
Liu, S., Nakajima, S.: Combining specification-based testing, correctness proof, and inspection for program verification in practice. In: Liu, S., Duan, Z. (eds.) SOFL+MSVL 2013. LNCS, vol. 8332, pp. 3–16. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-04915-1_1
Liu, S.: A tool supported testing method for reducing cost and improving quality. In: IEEE International Conference on Software Quality, Reliability and Security, pp. 448–455 (2016)
Liu, S.: Testing-based formal verification for theorems and its application in software specification verification. In: Aichernig, B.K.K., Furia, C.A.A. (eds.) TAP 2016. LNCS, vol. 9762, pp. 112–129. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41135-4_7
Liu, S., Ofiutt, A.J., Hostuart, C., Sun, Y., Ohba, M.: So: a formal engineering methodology for industrial applications. IEEE Trans. Softw. Eng. 24(1), 24–45 (1998)
Raimondi, F., Pecheur, C., Brat, G.: PDVer, a tool to verify PDDL planning domains. Computer (2009)
Lasalle, J., Bouquet, F., Legeard, B., Peureux, F.: SysML to UML model transformation for test generation purpose. ACM SIGSOFT Softw. Eng. Notes 36(1), 1–8 (2011)
Nayak, A., Samanta, D.: Synthesis of test scenarios using UML activity diagrams. Softw. Syst. Model. 10(1), 63–89 (2011)
Oluwagbemi, O., Asmuni, H.: Automatic generation of test cases from activity diagrams for UML based testing (UBT). Computer 77(13) 2015
Khurshid, S., Marinov, D.: TestEra: specification-based testing of Java programs using SAT. Autom. Softw. Eng. 11(4), 403–434 (2004)
Liu, S., Nakajima, S.: A decompositional approach to automatic test case generation based on formal specifications. In: International Conference on Secure Software Integration Reliability Improvement, pp. 147–155 (2010)
Liu, S., Hayashi, T., Takahashi, K., Kimura, K., Nakayama, T., Nakajima, S.: Automatic transformation from formal specifications to functional scenario forms for automatic test case generation. In: New Trends in Software Methodologies, TOOLS and Techniques Proceedings of the SoMeT 2010, Yokohama City, Japan, 29 September–1 October 2010, pp. 383–397 (2010)
Kent, S.: Model driven engineering. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 286–298. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-47884-1_16
Broy, M., Havelund, K., Kumar, R., Steffen, B.: Towards a unified view of modeling and programming (track summary). In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 3–10. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_1
Joseph, A.K., Radhamani, G., Kallimani, V.: Improving test efficiency through multiple criteria coverage-based test case prioritization using modified heuristic algorithm. In: International Conference on Computer and Information Sciences, pp. 430–435 (2016)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(1), 53–56 (1969)
Floyd, R.W.: Assigning meanings to programs. In: Colburn, T.R., Fetzer, J.H., Rankin, T.L. (eds.) Program Verification, pp. 65–81. Springer, Dordrecht (1993). https://doi.org/10.1007/978-94-011-1793-7_4
Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: Symposium on Foundations of Computer Science, pp. 109–121 (1976)
Yin, Y., Xu, Y., Miao, W., Chen, Y.: An automated test case generation approach based on activity diagrams of SysML. Int. J. Perform. Eng. 13(6), 922–936 (2017)
Acknowledgements
This work was supported by JSPS KAKENHI Grant Number 26240008, and Defense Industrial Technology Development Program JCKY 2016212B004-2. The authors would like to thank the anonymous referees for their valuable comments and suggestions.
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
Yin, Y., Liu, S., Chen, Y. (2019). Verification of SysML Activity Diagrams Using Hoare Logic and SOFL. In: Duan, Z., Liu, S., Tian, C., Nagoya, F. (eds) Structured Object-Oriented Formal Language and Method. SOFL+MSVL 2018. Lecture Notes in Computer Science(), vol 11392. Springer, Cham. https://doi.org/10.1007/978-3-030-13651-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-13651-2_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-13650-5
Online ISBN: 978-3-030-13651-2
eBook Packages: Computer ScienceComputer Science (R0)