VALIDATION AND VERIFICATION OF SYSML ACTIVITY DIAGRAMS USING HOARE LOGIC
Yufei Yin1 , Shaoying Liu1 and Yixiang Chen2
1Hosei University, Tokyo, Japan
2East China Normal University, Shanghai, China
Abstract
SysML diagrams are significant medium using for supporting software lifecycle management. The existing TBFV method is designed for error detection with full automation efficiency, only for code. For verifying the correctness of SysML diagram, we applying TBFV method into SysML diagram. In this paper, we propose a novel technique that makes use of Hoare Logic and testing to verify whether the SysML diagrams meet the requirement, called TBFV-M. This research can improve the correctness of SysML diagram, which is likely to significantly affect the reliability of the implementation. A case study is conducted to show its feasibility and used to illustrate how the proposed method is applied; and discussion on potential challenges to TBFV-M is also presented.
Keywords
SysML activity diagrams, TBFV, test path generation, formal verification of SysML diagram.
For More Details: http://aircconline.com/ijsea/V9N4/9418ijsea07.pdf
Comments
Post a Comment