Automated modeling of dynamic reliability block diagrams using colored Petri nets

Ryan Robidoux, Haiping Xu, Liudong Xing, Mengchu Zhou

Research output: Contribution to journalArticlepeer-review

100 Scopus citations

Abstract

Computer system reliability is conventionally modeled and analyzed using techniques such as fault tree analysis and reliability block diagrams (RBDs), which provide static representations of system reliability properties. A recent extension to RBDs, called dynamic RBDs (DRBD), defines a framework for modeling the dynamic reliability behavior of computer-based systems. However, analyzing a DRBD model in order to locate and identify design errors, such as a deadlock error or faulty state, is not trivial when done manually. A feasible approach to verifying it is to develop its formal model and then analyze it using programmatic methods. In this paper, we first define a reliability markup language that can be used to formally describe DRBD models. Then, we present an algorithm that automatically converts a DRBD model into a colored Petri net. We use a case study to illustrate the effectiveness of our approach and demonstrate how system properties of a DRBD model can be verified using an existing Petri net tool. Our formal modeling approach is compositional; thus, it provides a potential solution to automated verification of DRBD models.

Original languageEnglish (US)
Article number5340681
Pages (from-to)337-351
Number of pages15
JournalIEEE Transactions on Systems, Man, and Cybernetics Part A:Systems and Humans
Volume40
Issue number2
DOIs
StatePublished - Mar 2010

All Science Journal Classification (ASJC) codes

  • Software
  • Control and Systems Engineering
  • Human-Computer Interaction
  • Computer Science Applications
  • Electrical and Electronic Engineering

Keywords

  • Automated verification
  • Colored Petri net (CPN)
  • Deadlock detection
  • Extensible markup language (XML)
  • Formal modeling and analysis
  • Reliability block diagram (RBD)
  • System reliability
  • Time Petri net

Fingerprint

Dive into the research topics of 'Automated modeling of dynamic reliability block diagrams using colored Petri nets'. Together they form a unique fingerprint.

Cite this