5.7 モデル細分化手法の信頼性保証
5.7.2 操作の整合性保証
2.5節の式(2.5) にモデルの操作における証明責務を示した. この式のパラメタ制約C
とプロパティ制約Pを5.7.1項と同様の理由で省略し,QA∧IA⇒[VA]IAに注目する. 細 分化モデルの事前条件,不変条件, 代入をそれぞれQA0 , IA0, VA0 としたとき,操作に関する モデル細分化手法の信頼性を表す命題を式(5.8) に定義する.
(QA ∧IA ⇒[VA]IA)⇒(QA0 ∧IA0 ⇒[VA0]IA0) (5.8)
式(5.8)が成り立つことを証明2に示す. この証明では任意の変数間の関係を命題Pから
推論する推論器rsn(P)を想定する. 5.3節の制約条件展開がこの推論器の役割を担うが, 実際には理想的な推論器を実装することは不可能である. そのため, 操作の整合性保証は 制約条件展開に依存する.
証明 2 式(5.8)の証明
任意の変数間の関係を命題P から推論する推論器rsn(P)を想定する. この推論器を 用いたとき, X ⇒ Y が真であり, ある変数群v0 に関してX0 = chs(rsn(X),v0), Y0 = chs(rsn(Y),v0) であるならば, (X ⇒Y)⇒(X0 ⇒ Y0) は真である. これは, 推論器rsn によって変数群v0間の関係が推論された事で, v0 に関する命題Y0 を証明するのに必要 な仮定X0 が得られるためである. ここで, X をQA ∧ IA, Y を[VA]IAに置き換える事 では目的とする命題にはならないことに注意する. なぜなら, [VA0]IA0 が[VA]rsn(IA)に存 在しない命題を持つ場合にはY0 = chs(rsn(YA),v0)の前提が崩れるからである. [VA0]IA0 が[VA]rsn(IA)には存在しない命題を持つ場合とは, VAではy := y0 と変化した変数y がVA0 ではy := yとなり変化せず, IA0 が変数yを含む命題を持つ場合である. 5.5節の 制約条件抽出においてVAでは変化するがVA0 では変化しない変数をv0から除くことで [VA0]chs(rsn(I),v0)が[VA]rsn(IA)には存在しない命題を持たないようにしている. これ により, Y0 =chs(rsn(Y),v0)の前提が成り立ち式(5.8) が保証される.
第 6 章
モデル充足ソフトウェア合成
6.1 概要
本章ではモデル充足ソフトウェア合成(Model Satisfiable Software Synthesis, MSSS) を 提案する. MSSSはB Method のモデル(要求モデル)を入力として, 要求モデルに対す
る実装(合成実装)と要求モデルに実装依存の制約を加えたモデル(合成モデル)を出力す
る. 例として要求モデルとそれに対する合成モデルと合成実装の例を図6.1に示す. 以下 では要求モデルMK を式(6.1), 合成モデルMAを式(6.2) 合成実装MI を式(6.3) のよう に表す.
MK = (CK,PK,IK,UK,((QK1,VK1), . . . ,(QKl,VKl))) (6.1) MA= (CA,PA,IA,UA,((QA1,VA1), . . . ,(QAl,VAl))) (6.2) MI = (PI,RI,II,UI,(VI1, . . . ,VIl)) (6.3)
出力モデルMAは要求モデルMK に対して実装に必要な記述を追加したモデルである．
本手法では式(4.3)の細分化モデルと実装依存モデル間の拡張の定義と同様に，要求モデ ルと出力モデル間に式(6.4) が成り立つように合成する．式(6.4)は合成モデルの制約条 件が要求モデルに実装依存の制約条件を加えたものであり，初期化と操作の代入が等し いことを意味する．式(6.4)には事前条件についての記述が無いが，合成モデルの事前条 件QAj はQKj と同値またはより弱い制約に実装依存の制約を加えた命題である．これは 要求モデルの事前条件QKjが‘その条件において代入VKj が実行できる’という要求を表 すためである．
(CA⇒CK)∧(PA ⇒PK)∧(IA⇒IK)∧(UA=UK)∧(VAj =VKj) (6.4) MSFCの信頼性の定義である充足と同様に，式(6.4) に加えて出力モデルMAと出力実 装MI 間で式(2.4), 式(2.5), 式(2.6) の証明責務群を生成し, それらを証明することでソ フトウェアの信頼性を保証する. 本研究では式(6.4)，式(2.4), 式(2.5), 式(2.6)が成り立
61
第6章 モデル充足ソフトウェア合成 62
INVARIANT
persons <: 0..maxPerson &
groups <: 0..maxGroup &
belong : persons +-> groups CONSTRAINTS maxGroup:1..1000&
maxPerson:1..1000
OPERATIONS np<-- addPerson(group)=
PRE
max(persons)<=maxPerson-1&
group:groups VARIABLES persons, groups, belong MACHINE GroupManager (maxGroup,maxPerson)
INITIALISATION persons := {} || groups := {} ||
belong := {}
要求モデル
INVARIANT
persons <: 0..maxPerson &
groups <: 0..maxGroup &
belong : persons +-> groups &
CONSTRAINTS maxGroup:1..1000&
maxPerson:1..1000
OPERATIONS np<-- addPerson(group)=
PRE ...
VARIABLES persons, groups, belong MACHINE GroupManager (maxGroup,maxPerson)
INITIALISATION persons := {} || groups := {} ||
belong := {}
CONCRETE_VARIABLES A_fileOpen,
C_fileOpen, ...
A_fileOpen := TRUE ||
C_fileOpen := TRUE
THEN ANY person WHERE
person:0..maxPerson&
not(person:persons) THEN
persons := persons\/{person}||
belong := belong<+{person|->group}||
np := person END END;
合成モデル
INVARIANT
OPERATIONS np<-- addPerson(group)=
IMPORTS
persons.Set(0..maxPerson)
belong.PFun(0..maxPerson, 0..maxGroup) IMPLEMENTATION GroupManagerI (maxGroup,maxPerson) 合成実装
REFINES GroupManager
isEmp <-- persons_i.isEmpty;
IF isEmp = TRUE THEN newID := 1
ELSE
maxUID <-- persons_i.getMax;
newID := maxUID + 1 END;
persons_i.add(newID);
END;
VAR isEmp, maxUID, newID IN
W’a
Z’b Q’a
Q’b group:0..maxGroup &
C_fileOpen = TRUE A_fileOpen = TRUE &
C_fileOpen : BOOL & ...
A_fileOpen : BOOL & ... Ia Ib IK
QK
persons = persons_i.val &
A_fileOpen = persons_i.FileOpen &
belong = belong.val &
C_fileOpen = belong_i.FileOpen Ja
Jb
belong_i.setVal(newID, group);
np := newID
Z’c THEN
...
END;
VK
...
...
...
図 6.1: MSSSによるソフトウェア合成の入出力例
第6章 モデル充足ソフトウェア合成 63 つことをモデル充足と呼び，合成手法の信頼性の定義とする．この信頼性を満たす合成 を実現するために，本研究では要求モデルを細分化した検索キーによる健全性の高い部 品再利用を提案する．また，MSFCおよび 部品検索を数学的に定義することで，合成手 順で得られるソフトウェアの信頼性を定性的に評価し，モデル充足となる為に必要な人 間の証明作業を明確にする．
図6.2に示すようにMSSSの手順は大きく分けてモデル細分化，部品検索,変数名統一, 部品選択, 部品結合からなる. 以下に各手順を簡単に説明する．
1.モデル細分化: 要求モデルを機械的に細分化して4.2.1項で定義した細分化モデル群 を生成する．細分化モデルは部品の仕様であるため，これを検索キーとしてリポジ トリ内の細分化モデルを検索することで，小さな計算量で健全性の高い部品検索が できる．
2.部品検索: モデル細分化で得られた検索キーにより部品群を検索する. 詳細は6.2節 で述べるが，得られる部品が検索キーと同じ機能を有すること，また，検索キーで 与えられた条件下で実行可能な事を数学的な命題として与える．これを定理証明に 基づいて数学的に判定することで検索の健全性と完全性を保証できる.
3.変数名統一: 検索で得られた部品の変数名は部品間で異なるため，合成時に要求モデ ルを満たすように検索キーの変数名を用いて変数名を統一する．
4.部品選択: 要求モデルから得られた細分化モデル毎にたかだか１つの部品を選択す る. これは図6.2のように1つの細分化モデルに対して複数の部品が検索で得られる ためである. この際, I/Oなどの数学的には記述できない要求に応じて部品を選択す るため, 部品の記述を読解すること無く部品を選択できる仕組みを提案する.
5.部品結合: 部品の実装依存モデルを結合することで合成モデルを作り, 部品の細分化 実装を結合することで合成実装を作る.
MSSSの信頼性については9.2.1項で詳しく考察するが，要求モデルが実装依存の制約 条件を含まないならばモデル充足の式(6.4) を満たす合成モデルが得られる．また，要求 モデルが無矛盾であり，再利用した部品間に矛盾が無いならば，式(2.4),式(2.5), 式(2.6) の合成モデルの無矛盾性，及び合成モデルと実装間の整合性を保証できる．合成モデル の不変条件について簡単に説明すると，要求モデルの不変条件IK，その検索キーの不変 条件IKi，に対して，モデル細分化をIK ⇔ ∧
IKi と定義し，IKi と同値な不変条件を持 つ部品を検索するためである．これにより得られる部品の実装依存モデルの不変条件IDi は4.2.2項に示したように，IAi ⇒IKi であるため，∧
(IAi ⇒IKi)⇒ (∧
IAi ⇒∧
IKi) よ りIAi ⇒∧
IKi(⇔IK) となる．‘要求モデルが実装依存の制約条件を含まないならば’ と いう条件は細分化モデルは実装依存の制約を持たない為に生じる条件である．
部品検索では定理証明に基づき数学的に判定することで健全性と完全性を保証できる．
しかし，MSSSでは膨大な部品群を持つリポジトリを想定するため，部品数だけ定理証明
第6章 モデル充足ソフトウェア合成 64
図 6.2: モデル充足ソフトウェア合成の流れ
を繰り返すことは現実的ではない．そこで，本研究では数学的に等価な細分化モデルの 字面が等しくなるようにモデル細分化を構築し，部品数だけ繰り返す判定を文字列一致 で行うことを提案する．
得られた合成モデルと合成実装を B Method の枠組みで検証し，証明責務が真である
ならばComenC[8]などのコード生成器を用いて実行可能コードを得る. 証明責務が偽に
なる理由として‘部品選択時に部品を割り当てなかった細分化モデルが存在する’，‘選択し た部品間に矛盾する記述が存在する’ことが挙げられる．この様な場合には利用者による 部品の追加や部品選択のやり直しが必要となる．MSSSでは以下の作業を利用者が行う．
1.要求モデルの記述
2.細分化モデル群の無矛盾検証，および，矛盾時の制約条件の追加 3.部品選択における実装方法の選択
4.成果物に対する証明責務の証明，および，証明失敗時の修正
MSSSは検証作業や実装方法の選択などを検索時に行うため，既存の自動コード生成 よりも作業量が多いように見える．しかし，検証作業により成果物の信頼性を保証でき るためデバッグの手間を省くことが出来，また，手戻りを抑えることが出来るため，既 存手法より作業量が多いとは言えない．MSSSは利用者による実装方法の選択が必要であ るが，MSSSの入力はDSLなどの既存手法より抽象的であり, 既存手法においても仕様 記述時に実装方法を記述するため, MSSSの作業量が既存手法より多いとは言えない．
モデル細分化は5章で説明した．部品検索，部品選択，部品結合についてはそれぞれ 6.2節, 6.3節, 6.4節で説明する. なお，変数名統一は部品検索時に行うため，6.2節で合 わせて説明する．合成されたソフトウェアの証明責務が偽である場合の対応については 6.5節で説明する．また，モデル細分化の信頼性については5.7節で説明する．
第6章 モデル充足ソフトウェア合成 65