並行システムを解析するための逐次化と状態削減機能の実装: 仕様の自動生成を目指して

摘要

並行システムは逐次システムに比べてその全体の動作を把握することが難しい．そこで，並行システムが仕様を満たすことを判定するためのツールが利用されている．しかし，実際にはそのような仕様を記述することは，並行システムのモデル化よりも難しいことが多い．本報告書では，並行システムのモデルから仕様を自動生成するために，記号処理によって並行動作の逐次化と状態数削減をする手法を提案し，本手法を実装したツールについて報告する．%It is difficult to understand the whole behavior of concurrent systems comparing with sequential systems. Therefore, model checkers or theorem provers are used for verifying whether a model of a concurrent system satisfies a formal specification. However, describing such formal specifications is often more difficult than modeling systems. This paper presents methods to sequentialize concurrent behaviors and reduce the number of states based on a symbolic approach, for generating specifications, and shows an implementation of the methods.