図1: LTL_DLによる統合チェック
制御ソフトウェアと機械装置などの連続系を同時に表現するダイアグラム記法としてSysMLが提案されている。本年はSysML記述の整合性解析の問題について、情報の静的な構造と動的な振る舞いの両方を同時に自動検査する方法を考案し、自動検査の実験を行った。昨年度に調査したSMTソルバ・フレームワークOpenSMTに、「有界の集合と関係」を扱える理論ソルバを組込み、簡単な酒屋在庫問題についてのクラス図と状態遷移図からソフトウェア設計記述を得て、有界モデル検査を行った。その結果、既存の有界モデル検査ツールを使う場合に比べて、80～100倍大きな規模の問題を取り扱うことに成功した。
ソフトウェア工学におけるモデリングとはモデル記述を作成することであり、モデル記述とは開発上流工程で作成するソフトウェアの抽象的な記述である。プログラムを具体的な記述とする時、特定の観点から情報を捨象した抽象的な実体をモデル記述と呼ぶ。どのような観点を残すかによって、様々な種類のモデル記述がある。特定の観点からの記述によって、対象が持つ多様な観点、性質の把握を容易にする。
モデリングに対するこのような考え方は、UMLによって明らかにされた。実際、UMLはUnified Modeling Language の略であって、プログラミングとの対比によりモデリングと呼んだ。プログラミング言語に対するモデリング言語という概念の確立である。UMLは対象を表現する観点によって、クラス図、状態遷移図など、多様なモデル記述(ダイアグラム)からなるモデリング記法を提供するファミリ言語である、特に、クラス図は対象の静的な情報構造、状態遷移図は動的な振る舞いを書き表す。
モデリング記法各々は、特定の観点からの記述を与えるという利点がある反面、記述が独立になることから互いの関係つけ、記述間の整合性が問題となる。大規模なシステムを様々な観点から独立に記述できるということは、逆にその観点の間で整合性がとれているかが問題となるのである。ここでは、特に、クラス図と状態遷移図の統合に関する問題を取り扱う。クラス図と状態遷移図の表現に関して、各々の記述に向いた論理系を用いる。
UMLの考え方によると、クラスはオブジェクトの集合として解釈することができる。この時、クラスの継承関係は集合の包含関係となる。また、クラスとクラスの関係を表すアソシエーションは集合間の関係となる。すなわち、集合と関係を表現し解析する体系があれば良く、記述論理(Description Logic)を使う方法が提案されている。有界解析を適用する時には、集合の要素を有限とすれば良い。
状態遷移図で重要となる時相的な振る舞いは、たとえば、線形時相論理で表せる。実際、ロジック・モデル検査で、UMLステートダイアグラムを検証する方法などが提案されている 。
図1: LTL_DLによる統合チェック
文献[1]では、記述論理と線形時相論理を組み合わせた新しい論理系を提案し、有界解析する検証エンジンを開発して、専用検証エンジンの性能を評価した(図1を参照)。状態遷移の状態ごとに成り立つ性質を記述論理の式によって表現すること、状態遷移系列に関わる振る舞い性質を時相論理の式によって表した。たとえば、次のような式が成り立つか否かを有界モデル検査の方法で確認する。
ここで、性質fは「注文があって出荷されていなければ通知が出されている」を、性質f’は「注文があれば、次々状態で指定の状態に至る」ことを表す。従来のモデル検査ツールでは表現しにくい性質である。
図2: 全体像
本研究の全体像を図2に示す。クラス図と状態遷移図で書き表した設計記述から対象モデルM(LTL_DLモデル)を得る。一方、検証したい性質に関しては、クラス図が表現する側面からは記述論理(DL)、状態遷移図からは時相論理(LTL)の論理式として作成する。両者を組み合わせることで、統合チェックの検査項目をLTL_DLの論理式ψ(先に示したfやf’)として表現する。この時、モデル検査の問題は
が成り立つか否かを判定することになる。これは一般には決定不能になるので、有界モデル検査の問題として扱う。すなわち、有限の集合ならびに関係に限定し、また、状態遷移の深さを有限スコープ化する。LTL_DLの論理式ψは、記述論理の命題を含むことから、通常のSATベースの有界モデル検査で直接取り扱うことはできない。従来の方法では、(有限の)集合や関係を特性関数表現した上で、バイナリエンコーディング(真偽値で表現)していた。集合の要素数が増えると共に、検査対象の論理式が指数関数的に大きくなり、検査性能に大きな影響を与える。本研究では、SMTの枠組みを採用し、有界の集合と関係を取り扱う理論ソルバを開発する方針をとった。具体的には、昨年度調査を実施したOpenSMTフレームワークに新規開発した理論ソルバを組み込んだ。
実験では、開発したSMTソルバの有効性を確認することを目的として、既存SATソルバ(Yices)上でのバイナリエンコーディングによる方法と比較した。既存ソルバYicesはSATソルバとして用いた。Yicesは構造データを取り扱うことが可能なSMTソルバであるが、純粋なSAT機能のほうが高速である。その結果を図3に示す。
図3: 検証処理の実行性能
図3のグラフにおいて、縦軸は実行に要した時間、横軸は検査対象の問題規模を表すパラメータである。グラフから明らかなように、試作したSMTソルバはYicesに比べて、80～100倍大きな規模の検査対象を同等な処理時間で検査することができる。問題の構造を反映した専用の理論ソルバを用いることの効果が実証できたといえる。
以上、UMLのクラス図と状態遷移図を対象とした統合有界デル検査が実現できることがわかった。当初の目的であるSysMLに適用する場合、数値制約に関わる算術演算を取り扱う必要がある。線形算術演算の範囲であれば決定可能な理論ソルバを構築することができ、実際、OpenSMTにも基本理論ソルバとして組み込まれている。今後、線形算術理論ソルバと、今年度試作した有限の集合に関わる理論ソルバを統合する方式を検討することを計画している。