Modeling And Verification Of Embedded Real-time Software By Combination Of Visual Method And Formal Method

Embedded real-time system becomes more and more complicated with its widespread use in various domains. Every stage (from system analysis, design to implementation, verification) of embedded real-time software development is more difficult. In order to ensure embedded real-time software's safety and reliability, we provide a solution for verification and modeling of embedded real-time systems that combines UML based modeling and formal method based modeling. .UML2.0 sequence diagram is one of the most descriptive diagrams. It is highly intuitive and can clearly show the interaction among objects. However, it is not good at describing time requirement of real-time systems. In this paper we proposed a UML extended mechanism that not only can maintain UML 2.0's intelligibility but also can describe the time requirement of real-time software. We also proposed a method that can translate UML2.0 sequence diagram to timed automata. Then we can use UML2.0 sequence diagram to model embedded real-time software, and use timed automata verification tool to verify the model. Finally, we apply this method in an elevator controlling system.Our research can promote the development of modeling and verification of real-time embedded software, application of UML2.0 sequence diagrams and application of formal method.