H. Xu, L. Xing, and R. Robidoux
Reliability modelling, dynamic reliability block diagram (DRBD), coloured Petri net (CPN), formal verification, model checking
With the rapid advances of computer-based technology in mission-critical domains such as aerospace, military, and power industries, critical systems exhibit more complex, dependent, and dynamic behaviours. Such dynamic system behaviours cannot be fully captured by existing reliability modelling tools. In this paper, we introduce a new reliability modelling tool, called dynamic reliability block diagrams (DRBD), to model dynamic relationships between system components. Due to the complexity of DRBD models that involve dynamic conceptual modelling constructs, such as a state dependency (SDEP) block, design errors, which are subtle and difficult to detect, can be easily introduced during the modelling process. To formally verify and validate the correctness of a DRBD model, we propose a Petri net based approach by converting DRBD constructs into coloured Petri nets (CPN). We use a case study to illustrate how to convert a DRBD model into CPN, and how to use an existing Petri net tool to analyse and verify dynamic system behavioural properties. Our case study and experimental results show that DRBD models are a powerful tool for system reliability modelling, and our proposed verification approach can effectively ensure the correct design of DRBD models for complex and large-scale computer-based systems.
Important Links:
Go Back
