| Abstract: |
Real-time systems need to be correct with respect to both functional and timing behavior. 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. |
