Research And Implementation Of Time Requirement Analysis Based On CCSL

The complexity of real-time systems is increasing together with its rapid development in critical information arears,to solve the problem of how can we guarantee the safety of real-time system,keep them away from accident has become the emphasis in software engineering research.Nowadays,the work of software security analysis is mainly focused on the software requirements specification and functional design.However,in the actual process of software development,analysis and verification of time requirement is still weak,the time requirement generally in natural language or structured form of description,is difficult to directly convert to some kind of formal system.To solve the above problems,in this thesis we propose a real-time system safety verification method based on clock constraint specification language by using the model checking technology.This method further describes the primary time requirement through the clock constraint specification language,which provides convenience for the formal expression of time requirement.The main contents of this thesis are as follows:Firstly,to solve real-time system analysis and verification of time requirement,we put forward a kind of analysis framework stage for formal specification and verification of time requirement on software requirements.Secondly,with the help of EAST-ADL event chain model and TADL time constraints,we describe the time requirement for modal sequence diagrams with time constraint and event chain.Then we give a semantic mapping between event chain and CCSL specification.We design the time requirement classification table and the automatically construct CCSL specification algorithm based on the table and transformation rules.Thirdly,through timed automata and its model checking tool UPPAAL,formal modeling and verification of time requirements are completed.Firstly,the semantic mapping between the CCSL and the time automata elements are given,also several common expressions of the automata representation,then the attribute to verify the accessibility of time constraints as failure state,finally using the model checking tool UPPAAL to analysis and verify the time requirements.Finally,a case study of EBS(Electronic Brake System)is given and the method is proved to be viable and valid after achieving the verification step by step,so that a new thinking is provided.