Liveness Property Preserving Modeling Method For Safety-critical Systems

When developing Safety-Critical systems using traditional development methods,errors in early system design stage can be detected at the later stage of development,and the modification of system structure may cause a lot of time and human-source waste.However,the test stage in traditional development does not guarantee that there is no error in the system,which is important for SafetyCritical system.Correspondingly,the formal development method uses accurate mathematics language to describe system requirement,which is helpful to eliminate the ambiguity in natural language.At the same time,the formal method use mathematical proof to verify the correctness of model,which can discover the error in requirements and design stage of early development.However,using formal method in system development needs precise formal specification that translated from textual requirement,which is difficult for the developer.Therefore,it is necessary to use the requirement analysis method in requirement engineering to decompose the requirements,and transform it into a semi formalized intermediate language.This paper uses the SysML/KAOS method to deal with the requirement in the prophase,transforms the textual requirement into the goal that uses the specific markup language.Then decomposes the complex requirement according to the refined decomposition relation in the goal model to establish the hierarchy of the requirement.At the same time,the relationship mapping from the SysML/KAOS method to the formal modeling language Event-B is established,the goal and requirement refinement relationship in the goal model is transformed into the Event-B model elements,and then the correctness and consistency of the transformation are verified through the validation mechanism in Event-B.The main research work of this paper is as follows:Firstly,transforming the achieve goal of the functional requirements in the SYSML/KAOS model and the maintain goal which represent the safety requirements into the corresponding elements in the EVENT-B model.Then,three kinds of goal refinement patterns in the goal model are transformed into the Event-B model refinement relationship,and the transformation consistency and correctness proof are given.Finally,the problem of the loss of liveness property in the transformation is discussed.In this paper,the expression of liveness property in the Event-B modeling process is given,then the method of preserving the liveness property in the model is studied and the related proof is given in this paper.