A Method of Performance Analysis and Verification of Real-Time System Based on Model Checking

Performance analysis of software designs is particularly important for real-time system, quantitative analysis of a real-time system design allows the early detection of potential performance problems. This paper proposes a method of performance analysis and verification of real-time system which is based on model checking UML collaboration model. Firstly, task architecture of real-time system is created by an event sequence diagram which is based on a concurrent collaboration diagram. And then allocate time budget to the concurrent tasks in the system and convert the concurrent collaboration diagram to networks of timed automata in UPPAAL for automatic analysis and verification.