Expressing and Verifying Timing Requirements with UML

摘要

This paper presents a method of enhancing UML by dealing with timing requirements via statecharts. First, statecharts are converted to extended timed graphs (XTGs), in which timing requirements are expressed, later verified by a model checker. Statechart-to-XTG conversion is done manually, while XTG-to-model notation is automatic with a specially developed converter tool generating code for PMC model checker. The method has been successfully applied in verification of a railroad crossing system.