Requirements verification of real-time shutdown system by qualitative formalism

Hybrid real-time and embedded software development is an area where software requirements must be subject to highly rigorous and systematic analysis. This paper concentrates on the qualitative formal method to specify the continuous plant and the required system behavior in terms of languages based on the qualitative physics and to verify that the hybrid real-time system satisfies the required system behavior by a qualitative simulation. The qualitative reasoning approach is selected to help the designers concisely specify the desired system properties without having to describe unnecessary details. To demonstrate the effectiveness of using a qualitative formalism to specify and analyze requirements of embedded real-time software, we use a shutdown system (SDS) to illustrate how the software cost reduction (SCR) style specification can be transformed and analyzed