佐藤正和
広域状態遷移に着目した通信サービス仕様の検証
Abstract:通信サービスをソフトウェアで実現するにあたって，その信頼性を保つには，仕様記述の段階でその正当性が保証されることが望まれる．通信システムも他の計算機プログラムと同様，ある種の計算を実行する機械であるが，主として，1)状態遷移を伴う複数の主体が，2)信号の授受を通じて同期しながら，3）全体として特定のサービスを実現する，点に特徴があると言える．従って，仕様記述法もこれらの特徴を反映したものが使われる．
本稿では，通信サービスの仕様記述法として広域状態遷移ルール[1]と呼ばれる記法を用いた場合の検証法について述べる．
第2章では，通信サービス仕様の従来の記述法と検証技術全般について概観する．
第3章では，検証の対象としてSTRで書かれた仕様の可到達解析を取り上げ，そのアルゴリズムについて述べる．
従来の仕様記述法においては，可到達解析は特定の少数プロセスを対象としたものであったが，プロダクション
ルールによって広域状態遷移を記述する場合には，一般に不特定多数個のプロセスの存在を考慮する必要がある．こ
のとき，可到達状態を任意の複数のプロセスによって構成される到達可能な準広域状態として定義すると，可到達状
態集合の大きさは初期状態として与えるプロセス数に依存する．このため可到達性を一般に保証するには，プロセス数を無限と仮定した解析を行なう必要がある．ここでは，システムを構成するプロセス数と可到達集合の大きさの関
係を明らかにし，可到達状態集合の上限値の存在，およびその上限値を得るのに必要な最小のプロセス数を求める方
法を示した．これによって，無限プロセスの存在を仮定するシステムの可到達性を有限プロセスのそれに置き替えて
解析することが可能になった．
第4章では，第3章のアルゴリズムの高速化の手法を提案する．