Petri nets modeling in bag-theoretic relational algebra for large-scale systems analysis

Abstract

With the increased use of distributed processing in a wide range of applications, a need exists for techniques which can be used to assist in evaluating the correctness of concurrent software and hardware. In order to specify concurrent systems unambiguously and to be able to analyze such specifications, it is essential that specifiation languages have a firm mathematical foundation. Analysis of concurrent systems requires reasoning about the complete state space of the systems which is a difficult task, and is inevitably suspectable to human error. Thus, it must be supported by automated tools in order to be used effectively. Petri nets are a powerful modeling tool for studying such concurrent systems since they are suitable to express in a natural way parallelism, concurrency and non-determinism, and support verification of sytem properties such as safeness, liveness, reachability, and coverability. There are various analysis means for Petri nets such as the reachability anaysis, the invariant analysis, and reduction techniques. The major analysis technique is the reachability analysis because it is easily automated and performs the most thorough analysis. A major limitation in the analysis technique is explosion of a large states space in simulation. This problem can be alleviated by the relational approach. Database technologies may offer a formal basis for efficient management of large states space in generating a reachability tree. Moreover, tools for analyzing the reachability tree can be developed using the technologies. This thesis proposes a framework for modeling and analysis of Petri nets using relational database technologies. Within the framework, Petri nets and the reachability tree are formalized by relations defined in bag-theoretic relational algebra extended with some features. Analysis algorithms based on such formal relations are developed in the bag-theoretic relational algebra. Since semantics of Petri nets is based on bag theory, this ap...