ABSTRACT
The analysis and verification of the timing behavior is an important aspect in the model-based development of mechatronic systems. Components of a mechatronic system typically communicate and share data over a network which originates real-time requirements. The network introduced imperfections like package loss and delay have a stochastic nature and thus may lead to the violation of a real-time requirement which is considered as a timing error and has an impact on the system performance and reliability. The model-based timing analysis is a valuable task for the evaluation and prediction of the system reliability. Recently we introduced a method for the model-based analysis of timing errors. It comprises a mapping of a semi-formal baseline system model into a probabilistic model, namely a discrete-time Markov chain model. In this paper, we discuss the analysis of the Markov chain model with respect to the timing requirements with probabilistic model checking techniques. We use the probabilistic model checking tool PRISM and the probabilistic computation tree logic for the property specification. Model checking requires the appropriate transformation of the informal timing requirements to the temporal logic expressions. The verification results show whether a specific timing property is satisfied by the model or not and reveal design flaws in the early design phase. A model of a mobile medical patient table serves as a demonstrative case study.
