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 system properties such as safeness, liveness, reachability, and coverability. There are various analysis means for Petri nets such as the reachability analysis, 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 approach is quite natural. The framework has been realized in a commercial relational database system using a standard SQL. Thus, our framework exploits all advantages of the database system in management of complex data in a formal manner.
매우 다양한 응용 분야에서 분산 처리의 이용이 증가함으로서 컨커런트(concurrent) 소프트웨어, 하드웨어의 정확성을 검증하기 위해 사용될 수 있는 기술(Technique)에 대한 많은 요구가 있어 왔다. 컨커런트 시스템을 모호함이 없게 명세(Specification)하고 그런 시스템 명세을 분석할 수 있기 위해서는 시스템 명세 언어(Specification Language)가 확고한 수학적 토대를 가지는 것이 필수적이다. 컨커런트 시스템의 분석은 매우 어려운 작업인 분석하고자 하는 시스템의 전체적인 상태 공간 (State Space)에 대한 추론을 필요로 하고, 또한 사람 실수에 근본적으로 영향을 받기 쉽다. 그러므로, 컨커런트 시스템의 분석이 효과적으로 사용될 수 있기 위해서는 자동화된 툴(Tool)의 지원을 받아야 한다.
페트리네트은 자연스런 방법으로 병렬성(Parallelism), 동시성(Concurrency) 과 불명확성(Nondeterminism) 등을 표현할 수 있기 때문에 컨커런트 시스템을 연구하기 위한 강력한 모델링 툴로 알려져 왔다. 또한 페트리네트은 여러가지 시스템 속성들(Safeness, Liveness, Reachability, and Coverability)에 대한 해석 방법을 제공한다. 페트리네트의 해석 방법으로는 도달성 분석(Reachability Analysis) 기법, 불변성 분석(Invariant Analysis) 기법과 Reduction 기법등이 있다. 이러한 여러 분석 기법중 도달성 분석 기법이 가장 널리 사용되고 있다. 이유는 이 기법은 쉽게 자동화 될 수 있고 또한 가장 철저한 속성 분석이 가능하기 때문이다. 하지만 이 기법의 주요한 한계는 컨커런트 시스템의 전체 상태 공간의 폭발적인 증가에 있다. 이러한 문제는 관계 대수형 접근 방법으로 완화 시킬 수 있다. 데이타베이스 기술은 컨커런트 시스템의 전체 상태 공간을 표현하는 도달성 트리(Reachability Tree)를 생성하는 데 필요한 매우 많은 기억 용량의 효율적인 관리를 위한 형식론 적인 기초를 제공한다. 게다가, 도달성 트리를 분석하기 위한 여러 툴들도 그 기법을 사용하여 개발될 수 있다.
이 논문은 관계형 데이타베이스 기술을 사용하여 페트리네트의 모델링과 해석을 위한 틀(Framework)를 제시한다. 그러한 틀 내에서 페트리네트와 도달성 트리가 확장된 중복허용 관계대수형 대수에서 정의되는 릴레이션(Relation)에 의해 형식화 된다. 그러한 형식적인 릴레이션(Formal Relation)에 기초한 해석 알고리즘들이 중복허용 관계대수형 대수로 개발된다. 페트리네트의 의미론이 Bag 이론에 기초하였기 때문에, 이러한 접근방법은 매우 자연스럽다. 즉 Bag 이론상에서 모든 컨커런트 시스템 해석이 가능하게 된다. 이러한 틀은 표준 SQL를 사용하는 상용 데이타베이스 관리 시스템상에서 구현되었다. 그러므로, 우리의 틀은 형식론적인 관점에서 복잡한 데이타를 관리하는 데이타베이스 관리 시스템의 모든 잇점을 이용할 수 있다.
