|
Abstract: |
The increasing reliance on computer systems nowadays has resulted in a rapidly growing need to build reliable and fault resistant networks. Currently, computer system reliabilities are modeled and analyzed using techniques such as fault tree analysis (FTA) and reliability block diagrams (RBD). However, these methods can only provide static representations of system reliabilities, and cannot ensure the correctness of a system's dynamic reliabilities. Dynamic reliability block diagrams provide a framework for modeling the dynamic reliabilities of a system. However, validating the model involves locating and identifying deadlocks, faulty states and other system flaws which can become tedious when done manually. This thesis outlines an automated procedure for validating the reliability model of a computer system. The main focus of the procedure is an algorithm which converts a dynamic reliability block diagram (DRBD) into a colored Petri net (CPN) for the purpose of automatic DRBD model verification. By converting a DRBD model into a CPN it provides us the ability to automatically locate faults and deadlocks in the DRBD model by performing an analysis of the colored Petri net's state space.
We developed a prototype conversion tool based on our proposed conversion algorithm. In our prototype, a XML-based representation of a DRBD is used as input for the conversion algorithm, which converts the DRBD elements and structure into elements of a colored Petri net. The colored Petri net is stored using XML-based CPN file format, and can be verified using an existing Petri net tool, called CPN Tools.
|
