In: Journal of Systems and Software 57 (2), pages 155-174. June 2001.
Abstract: Real-time systems need to be correct with respect to both functional and timing behaviors. Specification and modeling methods for real-time systems must thus permit the evaluation of functional and timing properties. Conventional real-time schedulability analyzers and simulators are not based on a formal specification and a model can thus not be formally verified. Formal specifications, on the other hand, frequently ignore preemptive scheduling and resource access protocols and the results obtained are thus only of limited value for systems using state-of-the-art scheduling algorithms. This paper proposes a novel Petri net-based approach for constructing specifications that are both formally verifiable and operational. It presents a solution to the preemption problem and suggests a pragmatic generic real-time system model which can be easily transformed into models for formal verification of functionality and for scheduling simulation. The well-known mine drainage system case study is used to demonstrate the application of this approach.
Keywords: Real-time systems; Modeling; Patterns; Formal verification; Petri nets; Scheduling.