An integrated approach for specifying, modeling and verifying dynamic systems

This dissertation presents a three-phase integrated approach for Specifying, Modeling, and Verifying (SMV) dynamic systems. The problem is addressed from the perspective of computer automation, proving the feasibility of coupling a thorough bottom-up-like specification with various types of event/state space analysis.;The first phase of SMV is the specification of the system. Relevant characteristics subsuming elements such as: components, events, common-cause failures, and shocks, are specified. The specification uses a programming-language-like syntax called Reliability Descriptive Language (RDL).;In the second phase a model of the system is generated. In this phase, the RDL specification of the system is parsed and translated into a mathematical representation. This translation is performed by a compiler program that generates a new extension of Petri nets, termed reliability System Assessment Petri nets (RSA Pnets). From this RSA Pnet representation of the system, a state reachability generator program automatically synthesizes the event-sequences of the system.;During the third phase, the verification process of the system takes place. Here, dynamic aspects are analyzed using the state-space and the set of event-sequences generated in the previous phase. Several options for verifying the system are presented, explaining in detail the way in which the SMV paradigm can be "interfaced" with conventional and non-conventional existing verification approaches. Some of these verification possibilities are considered in detail. In particular, the dissertation discusses temporal-logic model-checking of reliability-oriented goals and hypertext-like browsing of the event-sequences. It is also shown how markovian analysis can be applied the reachability state-space generated by the second phase of SMV.