If Graphical Models Of Real-time Software Design Verification

Real-time systems are computer application systems which are timely response to external events occured randomly and finish on event handling fast enough. For real-time system, not only should it satisfy the correctness of logic, but also meet the correctness of the time. With time limit of system, the processing required in a certain time to finish. This requires real-time system must have a very high reliability. If the system malfunctions, it may cause serious consequences. Timed automata are effective calculation models descripting real-time system behavior. Analyzing real-time system design by Timed Automata, can effectively improve real-time system reliability.As a formal method, timed automata use the strict mathematical definition of the syntax and semantics of the standard language to describe the system, but formal method is straightforward and to grasp it is not easy. And visualization of modeling method is intuitive and easy to understand, which is widely used in the software development process. But it is lack of precise semantic and hard to modeling analysis and verification. If visualized modeling method could be combined with formal methods, it can provide good solution for real-time software modeling.This paper will be a real-time visualization software model combined with formalization and validation tools IF, to implement the modeling, the analysis and the design and validation process of real-time system. This paper first introduces real-time system software graphical design modeling element, modeling ideas and methods, then the system structure of IF, the description mode of real-time system by IF, the syntax and semantics of IF, and the real-time systems verification way and method using IF tools' components is studied. Through the analysis and comparison of real-time system software graphical design model and IF, we try to find both similarities, and give the mapping rules and methods, and the explanation which cannot be mapped. Finally, a practical example which implements real-time system graphical software design model mapping to IF is given, then the results are verified using the IF tool sets to detect whether real-time system modeling design meets the requirement.