Timing Requirement Description Diagrams for Real-Time System Verification

International audienceTURTLE is a real-time UML profile introduced a few years ago to address the analysis, design and deployment of time-constrained systems. The profile has a formal semantics. Further, it is supported by an open source toolkit: TTool. The latter enables formal verification of TURTLE models without specific knowledge of mathematical notations or formal languages. This paper proposes to extend TURTLE to cover the requirement capture phase, to check a model against formally expressed temporal requirements, and to achieve temporal requirement traceability. TURTLE is extended with SysML requirement diagrams. Non-formal and formal requirements are both handled. Timing Requirement Description Diagrams are introduced to formally express temporal requirements. TRDDs are based on UML Timing Diagrams. A Hybrid Power Management Unit of a Hybrid Vehicle serves as example