同時性を考慮した並行システムの振舞い検証に関する考察

摘要

並行システムのソフトウェア開発では，分散した複数のプロセスで同時に発生した事象を，漏れなく検知することが重要である．本研究の目的は，複数事象発生の同時性を考慮した，並行システム設計の振舞い検証を支援することである．本研究の基本的なアイデアは，並行システム全体の振舞いを区間の合成として定義し，同時性を区間内に局所化することである．本稿では，プロセス代数CSPを用いて並行システムの同時性を定義して，同時性を考慮した振舞い検証の枠組みを提示する．同時性の仕様記述を一般化してモジュール化することにより，同時性に関する仕様と検証の記述を容易にする．