Research And Implemention Of Model Based Real-time System Formalization Validation

With the development of computer technology,especially the application of real-time system in various areas,the features,which include function behavior,the resource utilization and energy consumption of real-time system in the field of software engineering,are getting more and more in-depth understanding.How to ensure the reliability of a real-time system during its model design phase becomes a focus of the field.During the process of system development,Unified Modeling Language(UML)has widely used by the designers.And it becomes the best choice for modeling the real-time system due to the excellent performance of the time diagram in time factor.However,UML is a half-formalized language which cannot be used to achieve the model verification directly.On the other hand,the timed automata model is a fully-formalized language,which can be employed by UPPAAL to achieve the real-time functional verification.Therefore,in this thesis the model of the real-time system is modeled by the timing diagram,and then transformed as the timed automata model in UPPAAL by the model transformation algorithm.In order to verify the real-time system,the formal verification method is proposed in this thesis,Firstly,we introduce the relevant theory and technology of the real-time system,give the formalized description of UML timing diagram and timed automata,and transform the timing diagram model into timed automata by improving the existing model transformation method.Then the functional behavior and the non-functional behavior are verified by the timed automata and its extension,respectively.In the extension,the formal definitions of resource and energy consumption timed automata are defined.According to the method mentioned above,the Real Time System Model Design(T-RTSMD)is implemented.In addition,the validity of the proposed method is verified by two examples of different application fields.