概要: ソフトウェア開発において品質保証は重要であり，そのための手法としてソフトウェアテストや欠陥の自動修正手法なと様々な手法が提案されている．しかし，ソフトウェアが修正すべき欠陥を含んでしまうのは，実装の段階だけとは限らない．例えば，仕様設計の段階でその原因が発生してしまう場合がある．開発が進み，そのような欠陥が実装を行う段階で発覚した場合，開発者は仕様設計の段階まで遡って修正し，再び実装しなければならなくなる場合もある．この場合，欠陥の修正にかかるコストは大きくなってしまう． 本研究は，仕様設計の段階で用いられるシーケンス図において欠陥を発見，および修正する手法を提案する．本研究が修正の対象とする欠陥は非同期モデルを表すシーケンス図において行われるメッセージ送受信の順序が逆転してしまうことによる欠陥とした．また，提案手法は発見した箇所が必ずしも修正すべきものとは限らないため，開発者に修正すべきかを確認しながら修正する半自動的な手法とした． 手法は，まずシーケンス図からモデル検査に用いるモデルを生成する．次にモデルに含まれるオブジェクト間で行われるメッセージのやり取りから，モデル検査のもうひとつの入力である検査式を生成する．ここで生成される検査式はオブジェクト毎に，そのオブジェクトに関連するメッセージの順序が逆転しないかをチェックするものである．そのためシーケンス図が含むオブジェクトとメッセージの数に応じて複数得られる．次に生成したモデルと検査式を用いてモデル検査を行う．この時，モデルが検査式に表された検査したい性質を満たさない場合，反例が得られる．反例が得られた場合には提案手法は開発者に対して，その反例が起こらないようにシーケンス図を修正する方法を提案する．これはシーケンス図に含まれる情報だけではこの修正方法を採用するかどうかを判断することはできないためである．そのため開発者に提案し，修正を適用するかどうかを選んでもらう．すべての検査式に対してモデル検査を行い，反例が出力されなくなれば終了する． 提案手法をツールとして実装し，いくつかのシーケンス図に適用して2種類の評価を行った．その結果，1つ目の評価ではシーケンス図が含むオブジェクトの数やメッセージの数に対して，提案手法の生成する修正案の数や実行時間を評価した． 2つ目の評価では実際の開発現場で用いられるシーケンス図に対して，ツールが出力する修正が正しいことが確認できた． タグ: Sequence, Diagram, Model, Checking, Linear, Temporal, Logic, XML

@mastersthesis{楠野明2015,
  author = {楠 野明},
  title = {非同期モデルのシーケンス図に含まれるメッセージ順序の曖昧性除去手法},
  school = {大阪大学},
  year = {2015},
  month = {feb}
}