An Embedded Real-Time Software Oriented Requirements Specification Language and Checking Methods

Abstract: Aiming at the requirements specification and related checking of embedded real-time software, a visual modeling language, RTRSM * (real-time requirements specification model*), which is compositional and based on hierarchical and concurrent finite state machine, is proposed. It uses state transitions with duration and scheduled events to describe timing constraints, and can support the description of interactivity and timing constraints effectively. Additionally, RITL (real-time interval temporal logic), a kind of prepositional temporal logic, is presented to make up for RTRSM*’s defect description of global system properties, which is the drawback of operational specification languages. Interpreted over timed state sequences, RITL is able to deal with the description of both point-based and interval-based metric temporal properties, and supports the property description of RTRSM * models naturally and comprehensively. The verification and validation of the resulted requirements specification, especially issues with respect to the reachability graph of RTRSM * models with finite system states and the simulation execution of the specification, are also explored. Key words: embedded real-time software; requirements specification language; requirements specification checking