Formal Analysis And Application Of Real-time Systems Based On UPPAAL And UML

When the Pervasive Computing age is coming,the real-time system will be more and more important. Productivity and quality of the real-time system are crucial for success of the real-time system.In order to ensure real-time system's safety and reliability,methods of analysis and verification of real-time systems that combines timed automata based on UPPAAL and UML are adopted in this paper.It is important to improve real-time systems'safety and reliability by adopting formal methods to carry on real-time systems analysis and designs.Timed automata is the main formal tools used in real-time systems'designs . Timed automata is an excellent graph-based notation for capturing timed control behaviour of systems.UML sequence diagram 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 adopted a UML extended mechanism that not only can maintain UML's intelligibility but also can describe the time requirement of real-time system.We also adopted a method that can translate UML sequence diagram to timed antomata.Then we can use UML sequence diagram to analysis real-time system,and use UPPAAL that is a timed automata verification tool to verify the model.Finally,we apply this method in a coffee controlling system and a traffic light controlling system.