形式手法を開発現場に持ち込むには -試験計画より始めよ-

全文

(1)ウィンターワークショップ 2016・イン・. 子. IPSJ/SIGSE Winter Workshop 2016 in Zushi (WWS2016). 形式手法を開発現場に持ち込むには —試験計画より始めよ— 山田隆弘† アブストラクト形式手法に対する興味は非常に高まっているが，形式手法がソフトウェア開発の現場で広く普及しているとは言い難い．本稿では，従来の開発手法と馴染みのある形で形式手法を導入するために，試験計画と形式仕様とを同時に作成するというアイディアを提示する．. How to Bring Formal Methods into Development - Start with Test Plans Takahiro Yamada† Abstract The formal methods are becoming well known among software developers, but they are still not used widely in software development. This paper proposes a method for introducing formal methods as a natural step in software development, which is to generate test plans and formal specifications concurrently.. 1. はじめに形式手法に対する興味は非常に高まっていて，その成功例もよく知られている[1]．しかし，それにもかかわらず，形式手法がソフトウェア開発の現場で広く普及しているとは言い難い．形式手法が現場で広まらない理由の一つは，形式手法を従来の開発手法の中にうまく組み込むための方法論がなく，形式手法を使用すると，その分だけ余分の労力（すなわち余分の費用）を投入しなければならないと思われていることであると思われる．本稿では，上記の問題を解決するために，従来の開発手法と馴染みのある形で形式手法を導入するための方法を提示する．具体的には，形式仕様と試験計画を同時に作成するという方法を提案し，その効用を説明する．. 2. 形式仕様の問題点人工衛星などの大規模システムを開発する場合，仕様を厳密に表現することが非常に重要になってくる．例えば，一つの人工衛星を開発する場合，たいていは百 †宇宙航空研究開発機構宇宙科学研究所． Japan Aerospace Exploration Agency, Institute of Space and Astronautical Science. c 2016 Information Processing Society of Japan ⃝. 人以上の技術者が関与する．開発を成功させるためには，それらの技術者の間で「どのような人工衛星を開発するのか」という情報が共有できていることが必須であり，そのようになっていないと，さまざまな不整合が発生する．従って，誰が読んでも同一の解釈に到達できるような仕様を作成することは，大規模システムの開発においては極めて重要である．形式手法は，まさに「誰が読んでも同一の解釈に到達できるような仕様を作成する」技術であり，大規模システムの開発で使用すべき技術であるが，実際にはほとんど使用されていない．その理由の一つは，形式手法は従来の開発手法にプラスしてなされるものであり，形式手法を使用すると，その分だけ余分の労力（すなわち余分の費用）を投入しなければならないと思われていることであると思われる．従って，形式手法を開発の現場において普及させるためには，従来の開発手法と馴染みのある形で形式手法を導入するための工夫が必要となる．. 3. 試験計画の問題点システム開発の最終段階において，開発されたシステムが仕様を満たしているかどうかを検証するために試験（テスト）を実施する．試験を実施するときには，試験の内容や手順を定義するために試験計画書や試験手. 7.

(2) ウィンターワークショップ 2016・イン・. 子. IPSJ/SIGSE Winter Workshop 2016 in Zushi (WWS2016). 順書を作成する（これらの文書名は分野によって異なるであろうが，ここでは宇宙分野で使用されている文書名を使用することにする）．試験計画書では，試験項目ごとに「システムのどの部分のどの機能（あるいは性能）をどのような構成（どのような治具をどのように接続するかも含む）で試験するか」を定義する．試験手順書では，試験項目ごとに試験を実施する手順（試験対象をどのような状態に設定し，どのような入力を与えて，どのような結果が得られるか）を定義する．試験はシステムが仕様を満たしているかどうかを検証するためのものであるから，本来は試験計画や試験手順は仕様に基づいて作成されるべきであるのだが，人工衛星開発の場合，そうなっていない場合が多い．その理由の一つは，仕様（特に要求仕様）が試験計画や試験手順を導出できるほどには詳細に定義されていないことである．もう一つの理由は，過去の人工衛星で使われた試験計画や試験手順をちょいちょいと手直しすれば，試験計画や試験手順が簡単に出来上がってしまうからである．実際のシステム開発では，試験計画や試験手順の作成に十分な時間が取れないことが多く，コピぺ・ベースの文書作成は，極めて普通である．しかし，これらの状況は改善すべきである．. 4. 形式仕様と試験計画の同時作成ここでは，形式仕様と試験計画（以降では，試験計画と試験手順の主要部分を総称して試験計画と呼ぶことにする）を同時に作成する方法を提案する．この方法には次に示す二つの利点がある．１番目の利点は，試験計画はシステム開発において必ず作成すべきものであるから，「形式手法はエクストラなものである」という誤解を払拭できることである．形式仕様と試験計画がいっしょに作成できれば一石二鳥であり，「お得感」が形成できれば形式手法に対する興味も高まるのではないかと期待できる．２番目の利点は，仕様の検証という真の意味での試験計画が作成できることであり，コピぺ・ベースの試験計画作成から脱することが可能となる．ただし，過去の開発における経験を活かすことは重要であり，コピぺ・ベースを完全に否定しているわけではない．次に，ここで提案する開発方法論を説明する．仕様には様々なレベルのものが存在するが，ここでは一つの例として，人工衛星に搭載されるデータ処理システムの要求仕様を考えることにする．搭載データ処理システムの要求仕様を作成するときには，その前提として，ミッション要求や（衛星全体に対する）システム要. c 2016 Information Processing Society of Japan ⃝. 求が定義されているのであるが，それらを満たすようにデータ処理システムの要求仕様を作成する．通常は，要求仕様は自然言語で記述するのであるが，なるべく厳密に，可能な限り形式的な言語を使って記述したい．そのために，各々の要求項目ごとに事前条件と事後条件を設定する．ここで提案する方法では，事前条件と事後条件の設定を行うときに「この要求を検証するためには，どのような試験を行うべきか」を考えるのである．すなわち，「この要求を検証するためには，システムをこのような状態にし，このような入力を与え，このような結果が得られることを確認すればよい」ということを考える．その中の「システムをこのような状態にし，このような入力を与え」の部分を事前条件として規定し，「このような結果が得られる」の部分を事後条件として規定すれば，形式仕様が得られる．これで，システムに対する要求仕様とシステム試験計画とが同時に得られることになる．一つのシステムは，たいていの場合，複数のコンポーネントから構成されているので，次のステップとして，システム仕様をコンポーネント仕様に分解する．この場合も，上述したのと同じ方法を適用し，「このコンポーネント要求を検証するためには，どのような単体試験を行うべきか」を考えることによってコンポーネントに対する要求仕様と単体試験計画とが同時に得られることになる．この後の開発方法は，従来の方法と同様であり，仕様に基づいて製造が行われ，試験計画に基づいて試験が実施される．. 5. おわりに本稿では，形式仕様と試験計画を同時に作成するという方法を提案し，その効用を説明した．この方法を用いると，「形式手法はエクストラなものである」という誤解を払拭できると期待しているのであるが，本稿の内容はまだアイディアの段階であり，実際の開発に適用したわけではない．このアイディアは，近いうちに実際の人工衛星開発に適用したいと考えているが，諸兄よりご助言やご批判を賜れば，幸いである．. 参考文献 [1]. 情報処理推進機構: 厳密な仕様記述における形式手法成功事例, 調査報告書 (2013). 8.

(3)