Automated Modeling of Dynamic Reliability Block Diagrams Using Colored Petri Nets
- 24 November 2009
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Systems, Man, and Cybernetics - Part A: Systems and Humans
- Vol. 40 (2), 337-351
- https://doi.org/10.1109/tsmca.2009.2034837
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.Keywords
This publication has 32 references indexed in Scilit:
- Explicit modeling of semantics associated with composite states in UML statechartsAutomated Software Engineering, 2006
- VERTAF: an application framework for the design and verification of embedded real-time softwareIEEE Transactions on Software Engineering, 2004
- Deadlock control methods in automated manufacturing systemsIEEE Transactions on Systems, Man, and Cybernetics - Part A: Systems and Humans, 2004
- Fault-Tolerant Deadlock Avoidance Algorithm for Assembly ProcessesIEEE Transactions on Systems, Man, and Cybernetics - Part A: Systems and Humans, 2004
- A framework for model-based design of agent-oriented softwareIEEE Transactions on Software Engineering, 2003
- Compositional time Petri nets and reduction rulesIEEE Transactions on Systems, Man, and Cybernetics, Part B (Cybernetics), 2000
- Object-Z: A specification language advocated for the description of standardsComputer Standards & Interfaces, 1995
- A unified high-level Petri net formalism for time-critical systemsIEEE Transactions on Software Engineering, 1991
- A Petri-net coordination model for an intelligent mobile robotIEEE Transactions on Systems, Man, and Cybernetics, 1991
- Petri nets: Properties, analysis and applicationsProceedings of the IEEE, 1989