Real-time and embedded system verification based on formal requirements

Abstract

TURTLE is a real-time UML profile supported by a toolkit which enables application of formal verification techniques to the analysis, design and deployment phases of systems design trajectory. This paper extends the TURTLE methodology with a requirement capture phase. SysML requirement diagrams are introduced. Temporal requirements (TR) are formally expressed using a dedicated language based on Allen’s interval algebra. TRs serve as starting point to automatically synthesize observers and to guide the verification process applied to the TURTLE model of the system. Verification results are automatically collected in traceability matrices. A Hybrid Sport Utility Vehicle serves as example.