Method Research On SysML Activity Diagrams Validation Based On Probability Model Checking

In recent years, as the complexity of system design creases, there are more and more errors coming up in the practical application of all kinds of system, which causes more and more serious incidents year by year. System modeling is now an essential link of various system designs,so improving the accuracy of the model is crucial to reducing various errors of the system which is generated later as the beginning of the entire system design process. Correctness analyzing and verifying to various models generated in the process of system design can find system bugs as early as possible, which can correct designing errors to reduce the occurrence of system problems.The so-called correctness of model designing refers to whether the designing model can correctly express certain functions and characteristics of future real system and if so then we can say that the model is correct. Model has been designed correctly or not is closely related to the availability and reliability of post-build real system.Systems Modeling Language(SysML) has been widely used by designing personnel in recent years as the standard modeling language in the field of software engineering and system engineering. SysML provides support for visual, graphical system modeling in the light of system designing and modeling in the field of system engineerng wherein the application of SysML activity diagram is used more widely. But because of its willing to keep the characteristics of comprehensible and efficient but simple modeling, it uses an semi- formal description method similar to UML which uses natural language in describing corresponding semantic, which determines the its own defect of lacking analyzing and verifying methods.Probabilistic model checking as an efficient, reliable and automated formal verification technology has particular advantages in the aspect of model validation. Therefore, how to verify the correctness of SysML activity diagram designing based on probabilistic model checking has been a research direction which is also the focus in this paper. The main work and innovation are as follows:1. This paper makes research on the semantic description of SysML. A method that represents formal semantic of SysML activity diagram based on new activity calculus is provided in the light of the defect of SysML activity diagram lacking precise semantic description. Firstly, this paper impro ves the corresponding activity calculus and adds the probability factor in the light of added probability elements in SysML activity diagram. Moreover, this paper gives the corresponding terms, definition syntax and operation semantic in the light of all the diagram icons in the new generated activity calculus to achieve the formal description of SysML activity diagram.2. This paper makes research on the method of achieving formal verification of Sys ML activity diagram in the software of PRISM model checking. Basing on the application object of model checking PRISM,,this paper gives the syntax and semantic of a kind of PRISM model, makes map to single diagram icon of SysML activity diagram represented in new generated activity calculus and gives detailed mapping rules, which makes the foundation of the conversion from SysML activity diagram to PRISM input language.3. This paper achieves a kind of algorithm making conversion from SysML activity diagram to PRISM input language. O n the basis of mapping rule s of single diagram defined above, this paper makes the codes to run in the model checking PRISM, gives the rules of expressing natures using PCTL probabilistic sequential logic and makes the corresponding model codes and the natures needing to be met as two inputs to the software of PRISM probabilistic model checking to realize the verification of whether the model design of SysML activity diagram is correct or not by making use of the conversion algorithm.4. This paper makes verification on the model of SysML activity diagram in the system of interactive learning and training on the basis of theoretical research. This paper achieves the conversion of activity diagram and the description of PCTL natures and verifies the feasibility and effectiveness of the method provided in this paper by running the model checking PRISM according to the validation method provided above, which opens up a new way of making verification on the model of SysML activity diagram.