Requirement Analysis And Verification Based On SysML Model

Model-Based Systems Engineering(MBSE)is often used to develop large-scale software systems to improve the reliability of software.Systems Modeling Language(SysML)is a standard modeling language used in MBSE.It is used for requirement analysis,design,coding,testing and other activities while supporting s Systems Engineering.SysML model is also often used in software code design.Therefore,whether SysML model accurately expresses users ‘needs become the key to high reliability of software code.However,few algorithms or tools can formally support requirement analysis and validation of SysML models,especially those based on unstructured SysML models.This thesis chooses SysML activity diagram model which has the ability to describe the dynamic behavior of the system as the research object,and innovatively proposes a formal verification method based on test cases(Testing-Based Formal Verification for Model,TBFV-M)to verify whether the SysML activity diagram meets the needs of users.The main work of this paper is divided into the following three aspects:(1)Design a test case generation algorithm based on unstructured SysML activity diagram.The TBFV-M method is based on test cases.This algorithm improves the limitation that the current mainstream generation algorithms can only be applied to structured activity diagrams.It transforms unstructured activity diagrams into an intermediate representation,and automatically generates test paths according to the intermediate representation.Finally,test data is generated according to the data constraints of the test path.(2)Propose a formal method based on test cases to verify whether SysML activity diagrams meet users' needs.TBFV-M method uses user requirement specifications and SysML activity diagrams as input,and uses Hoare Logic to verify whether each test path of SysML activity diagrams accurately describes the corresponding functional requirements.This method has the ability to detect and locate requirements description errors in SysML activity diagrams,and to prove that SysML activity diagrams accurately model user requirements.(3)Develop a requirement analysis and verification tool based on SysML activity diagram.The tool implements the TBFV-M method.When users use the tool,they input SysML activity diagram and user requirement specification,which can automatically generate test cases and validate requirements for SysML activity diagram.Finally,the validation tool developed in this paper is proved to be practical and effective in practical application through the drug sales system.