8.1.1 制御容易性の評価
評価目的
制御容易性の評価を行う．具体的には，モデルを変更するにあたって，追加，変 更する箇所の数を比べて，どちらが局所的になっているか評価する．
評価方法
検査モデルに対して，次の変更を行う．
• 呼び出すメソッドの変更
• アサーションの挿入
例えば，図8.4の車内ライティングシステムの場合を考える．事例の詳細につい ては，8.2節で後述する．メソッドSPLをメソッドSPL2に変更することを考える．
例として，図8.1に示すBSAVERクラスのステートマシン図で考える．
図 8.1: BSAVERクラスのステートマシン図 変更後は図8.2のようになる．
図 8.2: 変更後
これを本稿で提案しているアスペクトを利用した変更手法を利用すると，図8.3 のように記述できる．
図 8.3: アスペクの記述
以上のように，この場合だと手動で変更すると6箇所の変更が必要だが，アス ペクトを用いると１つのアスペクトを記述するだけで対応ができる．本手法を利 用しない場合とした場合の記述箇所の数を比べ，評価する．
8.1.2 観測容易性の評価
評価目的
観測容易性の評価を行う．具体的には，LTLの述語の定義に参照される変数，ラ ベル，演算子の数を比較し，どちらが単純に定義できているか評価する．
評価方法
モデル化の仕方によって，事象の観測する方法が違う．検証のことを考慮せず モデル化すると複雑な観測方法になる場合がある．
例えば，以下の述語は同じ事象を意味しているとする．
#define p (x>=10) && (x<=20) && C1@L1
#define p state1
以上のように，この場合だと上の述語は，変数2つ，演算子4つ，ラベル1つで あるのに対し，下の述語は変数が1つであり，より下の述語のほうが単純に定義 ができていると言える．このような，述語の定義の複雑さの違いを評価する．
8.1.3 簡潔性の評価
評価目的
簡潔性の評価を行う．具体的には，LTL自体の項と演算子の数を比較し，どち らが簡潔に定義できているか評価する．
評価方法
次に，簡潔性ではLTL式自体の複雑さを評価する．例えば，以下のようなLTL を考える．
À
(((!q && !r && !s && !t && !u) U p) && ((!r && !s && !t && !u ) U q) && ((!s && !t && !u ) U r)
&& ((!t && !u ) U s) && (( !u ) U t) && <>u
Á
(!q U p) && (!r U q)
&& (!s U r) && (!t U s) && (!u U t) && <>u
À
とÁ
は同じ意味のLTLである．しかし，À
の項は21個，演算子は36個，Á
の項は10個，演算子は16個であり，