ソフトウェア工学

ソフトウェア工学とは

いままでのソフトウェア開発では、技術者の経験や勘に頼る部分が多くありました。 しかし近年のソフトウェアの大規模化による開発環境の分散や開発人数の増大のため、 経験や勘にばかり頼っているわけにはいかなくなってきています。

ソフトウェア工学とは、 そのような職人芸的な部分を定式化し、 品質の高いソフトウェアを開発する方法論を確立するための学問です。 一言で言えば 「高品質のソフトウェアを如何に効率よく作るか」 ということを研究していると言えます。

ソフトウェアのライフサイクル

ソフトウェアの需要が生まれてから、 使命を終え破棄されるまでの流れをソフトウェアのライフサイクルと言います。 下図は典型的なライフサイクルのモデル、ウォータフォールモデルです。

ウォータフォールモデルの図

この他にも様々なライフサイクルのモデルがありますが、 ほとんどのソフトウェア開発は上流工程の生成物を 下流工程においてリソースとして用います。

ソフトウェア開発のコスト

ソフトウェア開発のコスト(時間、労力、費用)は人の作業量によって決まります。 人の作業量はソフトウェアの規模によって変化しますが、 それとともに誤りの混入によっても増加します。

ある工程において誤りが発見された場合、 誤りが混入していたリソースを生成した工程まで戻り、 誤った部分を破棄して作りなおさなくてはなりません。 大規模なソフトウェア開発では、 誤りの修正は作業中の他の人に大きな影響を与えます。 そのためこのような手戻りを少なくすることが開発コストを抑えるために必要です。

織田研における取り組み

誤り修正による開発コストの増加を抑制するには、以下のことが有効と考えられます。

  • 各工程での生成物に、誤りを混入させないこと
  • 各工程で誤りのない(高品質な)リソースを使用すること
  • 混入してしまった誤りは早期に発見すること
  • 誤りは人が行う作業により混入するので、可能な限り自動化すること
  • 信頼できる過去の生成物を積極的に活用すること

仕様の検証

要求定義と形式的仕様記述

ソフトウェアの開発は、 まず顧客が求める機能を導出し定義すること (要求定義)から始まります。 開発はこの工程で得られた仕様を基に行なわれるため、 開発全体のコストを減らすためには 誤りの無い仕様を作成することは特に重要と言えます。

仕様を記述するために、 データフロー図や状態遷移図などを用いる方法がありますが、 仕様に誤りがないことを保証するには証明が必要です。 仕様の証明を可能とするためには記述の意味が一意に定まる (形式的である)必要があります。 そのような記述を行なうための言語が形式的仕様記述言語です。

仕様の誤りには矛盾、曖昧さ、冗長、非妥当などがありますが、 形式的記述を行なうことで曖昧さが排除され、 矛盾する箇所、冗長な記述を検出することができるようになります。

正しい仕様を得るために

形式的仕様記述を行なうことで、仕様中の数学的な誤りが検出できます。 しかし、正しい仕様とは数学的な誤りを含まないだけでなく、 要求を確実に満たしている必要があります。 ところが、見落としなどにより十分な記述が行われず、 これにより発生した意図しない動作が他の制約に矛盾しなかった場合、 その仕様は無矛盾ですが要求に対して妥当だとは言えません。 そこで、織田研究室では次のような研究を行なっています。

妥当性検証の着眼点

仕様が要求を漏れなく満たしていること、 つまり妥当であることを確認するためには仕様と要求の比較が必要です。 しかし、実際の要求は人の頭の中にあるため、 このままでは比較は不可能です。

要求を形式的に記述する作業は、 使用する仕様記述言語の計算モデルに要求を落し込むことを意味します。 また計算モデルには複数の種類が存在し、それぞれ実世界の捉え方が異なります。 捉え方が全く異なる場合、 モデルへの落し込み作業において見落としやすい項目に違いがあると考えられます。 妥当性は単一のモデルは検証できませんが、 人為的なミスの発生原因に着目した場合、 要求を計算モデルの異なる 2つ以上の言語を用いて記述すれば、 そのモデル間の矛盾を調べることで非妥当な記述の一部を発見できる可能性があります。

モデル比較に基づく部分妥当性検証

織田研究室では、 近年広まりを見せている集合論に基づく仕様記述言語 (Z, B, VDM など) を対象とした 妥当性検証法を研究しています。

以下は Z で記述した自動販売機システムの一部です。 集合論に基づく仕様記述言語では、 システムが常に満たすべき条件や 操作を適用した際に集合(変数)にどのような変化が発生するかを記述します。

抽象的状態のスキーマ 操作のスキーマ

Z では操作前後の変数の値がシステムの不変条件に違反しないことは検証できますが、 システムの振る舞い(変数の変化)が要求に則しているかどうかは検証できません。 1つの操作で複数の変数が同時に変化し、 その記述が十分かどうかを一目で把握しにくいと言えます。 Z の記述は操作を基準としていますが、 変数の多くは実世界の対象(エンティティ)を表現しているため、 そのエンティティ単位の振る舞いに着目した異なるモデルを用意し比較すれば、 見落としによる記述不足等の発見が期待できます。

たとえば、自動販売機の商品というエンティティに関して 以下の状態遷移図を用意したとします。 これは非常に簡単なモデルですが、 Z の記述不足の発見に非常に有効に機能します。 Z の記述チームと、 状態遷移図の記述チームを分離するとさらに良い性能が期待できます。

こうした異なるモデルの比較では、 互いに対応する要素の決定が重要な課題です。 集合論による記述の中には状態名が存在しませんし、 人による対応付けに頼った手法では信頼性が低くなります。

織田研究室では、 信頼できる対応付けの推論手法、 モデル間の差異の計算とそれに基づく仕様上の誤りの推論、 これらを自動的に行なう検証器の実装などを研究し、 仕様の妥当性の保証を目指しています。


ソースコード自動合成

自動コード生成

自動コード生成とは仕様や設計から自動でソースコードを生成する事です. これにより, 人間がプログラミングという作業から解放されると同時に 人間のミスによって生じてきたバグを解消することにもつながります. これを実現するためには「手段を発想する」という 人間が行ってきた創造的な活動を補う必要があります. このために多くのアプローチが試みられてきました. これまでのアプローチを大きく分類すると 「再利用」に基づく方法と「人工知能」に基づく方法に分けられます.

ソフトウェアの実装の概念図

再利用と自動コード生成

「誰でも出来る事でも最初に実行することが難しい」 これを表す逸話としてはコロンブスの卵が有名です. 創造的な活動も最初の一人が行えば, それを見て後に続くだけならば創造力を要しない. これはソフトウェアにおいても言えることです. 手段を創造することは計算機には出来ませんが, 人間が創造した手段を繰り返す事は計算機にも可能です. 一度創造された手段を「部品」として再利用することで今までに無いソフトウェアを計算機に作らせる. これが再利用による自動コード生成で, 既に多くの開発現場で用いられています.

しかし, 部品の創造は人間に頼り, さらにそれが多くの場面で繰り返されるため, 部品にミスが含まれていると問題がとても大きくなります. また, 業務の分野毎に必要な部品が異なるため, 新たな分野で自動生成を行う事は非常に大きな労力を必要とします.

人工知能と自動コード生成

計算機に創造的な活動を行わせようという試みとして人工知能があります. 計算機に数学的に記述された仕様を与え, それを満たすソフトウェアを計算機に導かせる. これは人間が「創造」によって得る数学の答えを計算機に 「発見」させる事によって実現します. この方法はプログラミングを数学の問題として捕らえることで, プログラミングのミスが発生しません. まさに夢のような方法と言えるでしょう.

しかし, これを実現するためには砂漠から 一粒の砂金を得るような膨大な時間を必要とします.

織田研での取り組み

再利用と人工知能による自動コード生成にはそれぞれ長所短所があります. これらの長所をあわせ持った自動コード生成は出来ないのでしょうか?

織田研究室ではこれに対するアプローチとして 形式手法 B Method を応用した自動コード合成を提案しています. B Method は抽象的な仕様記述から実行可能な実装までをサポートした形式手法です. B Methodを用いる事で, 実装が仕様を満たすことを数学的な証明によって保証することができます. この B Method の枠組みで部品を構築することで部品の信頼性を保証することが出来, また, 部品の仕様が数学的に記述されていることで健全な再利用が可能になります.

コード合成の概念図

織田研究室ではさらに, 高信頼部品の自動生成にも取り組んでいます. これによって分野に捕らわれること無く手法を適用することが出来るようになります.

細分化部品登録の概念図

このような自動化技術においては どこまで自動化出来るのか, 信頼性はどこまで保証出来るのか, コードを得るのにどれくらい時間がかかるのかが問題になります. 織田研究室では 数学的判定の文字列一致判定による代替や 手法自体に対する数学的保証などを研究し より効果的な自動コード生成を目指しています.

このようなソフトウェア開発の自動化技術が実用化されれば 開発現場の構造は大きく変化する事でしょう. 人間によるバグの混入を防げることも大きな利点ですが, なによりも, 人間はより創造的な仕事に専念できるようになるでしょう.

電気通信大学 情報理工学研究科 情報学科専攻 織田研究室