装置を制御するプログラムは、複雑化の一途をたどっているが、複雑なソフトウェアを、高い信頼性を維持しながら開発する手法は、確立しているとは言いがたい。

　制御ソフトウェアは、機械装置という非決定性を持つものを対象としているため、障害の再現性がなく、潜在的なエラーを見つけ出すことが難しい。通常よく用いられるテストによる信頼性の向上は、相手がコンピュータよりはるかに遅い機械であること、テスト自体が危険を伴うことなどから、思うように成果をあげられない。また、開発リソース、開発期間は不十分で、十分なシミュレーション、机上デバッグを行えないケースが多い。

　一方、機械設計においては、以前から「先輩の設計をまねて、一部だけを変える」ことが一般的であった。これと同様に、ソフトウェアにおいても、修正が安全に実行できたら、上記の問題が大いに改善される。しかし、仕様変更に対応してソフトウェアの一部分だけを変更する場合は、その変更が、ソフトウェアの他の部分に影響を及ぼさないかどうかを調べる必要がある。そこで、

　順方向のパス 要求される機能の変化に対応して、プログラムを変更する方法があること。

　逆方向のパス 変更されたプログラムが、どのような機能の差をもたらすか、調べる方法があること。

　これら二つの条件を満足する設計手法を、差分駆動型設計と呼ぶことにする。本研究においては、いままであまり研究されていなかった逆方向のパスを中心に、制御ソフトウェアの特殊性に合った、安全な差分駆動型設計を実現するための手法を提案する。

　装置を制御するプログラムは、多くのアクチュエータを同時に扱うため、並行性が要求される。一方、各々のアクチュエータの制御プロセスは、比較的単純である。このように単純なプロセスの並行動作に適したプログラミングモデルに、CSP(Communicating Sequential Processes)がある。CSPは、複数の互いに通信しあうプロセス群を数式で表現したものであり、プロセスを扱うための多くの演算が含まれている。ここでは、ガード、決定的OR、非決定的OR、隠蔽、並行動作という4つの演算だけからなる、制限された(Reduced)CSPモデル(以後、RCSPモデルと呼ぶ)を使用する。

　図1のプレス装置を、RCSPモデルで表現した例を図2に示す。この装置は、金型を使ってテープから製品を打ち抜き、その製品を動かないように真空吸着するものとする。装置にはプレスシリンダ、真空吸着用の弁という二つのアクチュエータと、動作確認用のセンサが付いている。

図1:Press

図2:RCSP notation of press machine

　制御ソフトウェアでは、並行動作するプロセスの数が多いため、デッドロックや無限追い越しなどの障害が起きるケースが多い。幸い、RCSPモデルに対しては、デッドロックなどを検出する検証系として、Spinなどが利用できる。Spinはプロセス群の通信を網羅的に検査し、イベントの同期がとれずにデッドロックする箇所を指摘する。たとえば、前述のプレス装置で、わざとデッドロックを起こすようにしたものをSpinを使って検証すると、図3のように、デッドロックが起きる箇所での、各プロセスの状態を表示する。

図3:Deadlock detection by Spin

　このように、Spinによる検証は大変有用であるが、プログラムの規模が大きくなると、Spinの要求するメモリ、計算時間は指数関数的に増大する。図4に、似たようなプレスを1台持つ装置から、4台持つ装置までをSpinで検証した際、必要であったメモリ容量を示す。この結果から、大規模な装置をSpinで検証するのは容易ではないことがわかる。

図4:Required memory for verification

　実際のソフトウェア開発では、様々な小変更が発生する。そのたびにソフトウェア全体を検証するのではなく、変更された部分と、変更に影響される部分だけを検証することができれば、実用的な時間内で検証が可能になる。

　RCSPモデルにおいては、イベントの共有関係を介して変更の影響が伝搬していく。たとえば、図5でPRESSが変更されると、まずCUTがその影響を受け、CUTを通じて間接的にHOLDが影響される。ところが、隣接したプロセスが変更されても、全く影響を受けない場合がある。たとえば、PRESSが変更されたにもかかわらず、PRESSの、CUTから見た振舞いが、以前と全く同じであったら、変更はPRESS内部だけに留まり、CUTは影響されない。また、CUTを介して、その影響が隣接する他のプロセスに伝搬することもない。このような状態を、変更がPRESSからCUTに伝わる時に「ブロックされた」と呼ぶことにする。

図5:Press processes

　変更前後のプロセスから、共有されるイベント以外を隠蔽し、比較すると、ブロックの有無を判定できる。この手続きをプログラムとして実行した例を図6に示す。隠蔽後のプロセスの振舞いが同じなので、変更はブロックされていることがわかる。このようなプログラムを利用して、変更の影響を追跡することができる。

図6:Determination of blocking

　RCSPモデルを用いた制御ソフトウェアの開発においては、モデルを検証用、影響追跡用、実行用の言語に書き直す必要がある。この書き直しによるコスト増大と、書き直しのミスを防ぐため、一つのソースファイルから上記三言語およびドキュメント用のL^AT_EXへの自動変換を行う開発環境を作成した。本環境では、オリジナルのソースをSGMLで記述し、それをSGML Parserやawkなどのツールを使って、様々な言語に変換する。この方法によれば、たとえば、検証したモデルと制御プログラムが同一であることが保証できる。

　この開発環境を用いて、四台の装置の制御プログラムを作成したが、その中の一台で、開発中に大きな仕様変更があり、実際に影響の伝搬を追跡するチャンスがあった。

　変更前のプロセスの一部を図7に、変更後を図8に示す。UPSTOCKUD2、STOPPER2が新設され、LOWSTOCK、STACKERが変更された。これらの変更の影響を追跡したところ、UPSTOCKのみが影響を受け、TRAYCLAWなど他のプロセスへの伝搬はブロックされることがわかった。

図7:Process graph before modifications

図8:Process graph after modifications

　本研究は、制御ソフトウェアの設計において、仕様の変更に対応してプログラムの一部分を変更するための、開発効率、信頼性の両面から満足できる手法を確立することを目的としている。

　機械装置を制御するソフトウェアの開発においては、頻繁な仕様変更に対しても、高い信頼性を維持しつつ、短期間にプログラムを設計することが求められる。既存の設計例をもとに、仕様変更部分に対応するプログラムの一部分を変更する、すなわち差分設計を行うことで、設計期間の短縮が予想されるが、そのためには、変更のプロセスで信頼性が維持できることを保証しなければならない。本論文の提出者は、製造装置を開発するセクションに勤務し、開発手法を自ら実践的に評価しうる立場にある。本論文では、HoareのCSPを制限した独自のプログラミングモデル上の差分設計が、上記効率性、信頼性の条件を満たすものと主張し、ICを製造する装置に適用することで、その効果を実証しようとしている。

　機械装置の仕様変更は、アクチュエータの追加、変更などと、それに伴う動作順序の変更などといった形で提示される。従って、アクチュエータ、動作順序などと対応するようにプログラムの構造を記述すれば、仕様変更とプログラムの変更とがよく対応すると予想される。本論文では、CSPを制限したモデルがこの目的に適していると主張しているが、これを確かめるため、上記IC製造装置で、実際にこのモデルを用いた設計を行い、できあがったモデルから制御プログラムを導出して、装置を制御した。その後、この装置で大きな仕様変更があり、本手法の有効性が試される機会があったが、仕様の変更と、モデルの変更はほぼ一対一に対応したと報告されている。

　機械を相手とする制御ソフトウェアでは、実際に機械を動かしてのテストが危険かつ困難であるため、事前の動作検証が必要になる。ここでは上記プログラミングモデルを、デッドロックなどを未然に発見するためのモデルとしても利用している。しかし、制御ソフトウェアでは入力が数十から数百と多いために、自動検証が事実上不可能であるという問題がある。この問題を解決するためには、モデルを階層的に分割し、段階的に検証を進める方法をとっている。

　モデルを階層的に分割することは集中力を要する作業である。また、人手が介在するためにミスが入り込む可能性がある。本論文では、モデルの一部の変更の影響が、モデル内をどのように伝播していくかを追跡する方法を開発し、検証の範囲を限定することに成功した。この結果、いったん検証が完了したモデルを変更する際には、人手を介することなく、モデルを自動検証することが可能になった。

　このように、変更の影響を追跡する手法は、従来の差分設計にはない、新しいアプローチである。従来の手法では、仕様変更に対してプログラムやモデルを変更する方法は提供されていても、変更の結果がプログラム全体に対してどのような影響を及ぼすかを評価する方法はなかった。そのため、高い信頼性を得ようとすると、変更のたびにモデル全体を検証し直す必要があった。

　本手法では、一つのプログラミングモデルから制御プログラム、検証用モデル、変更の影響伝播追跡用モデルなどを導くことで、安全な差分設計を実施できるとしているが、そのためには、もととなるモデルと、導出されたプログラムなどが等価であることを保証する必要がある。この目的のため、単一のモデル記述からプログラムや他のモデル、ドキュメントなどを自動生成するシステムを開発した。なお、このシステムによる波及効果として、モデル間の変換に要する時間が不要になることにより、開発期間が短縮された。

　ここで提示された設計手法は、合計四台の装置の開発に適用され、できあがったプログラムの信頼性、仕様変更に対する即応性、デッドロックの検出などに対して高い評価を受けたと報告されている。これらの結果から、本手法は開発効率、信頼性ともに高く、初期の研究目的を達したと判断できる。

　機械装置の制御ソフトウェアという分野は、ソフトウェアエラーが直接人間、社会に対して影響を及ぼす点で、信頼性に対する要求が厳しいが、リアルタイム性、入力の多さなど、その特異な性質から、従来ソフトウェアエンジニアリングの対象になりにくかった。本論は、この分野に差分設計の手法を導入し、さらに、変更の影響を追跡することで、差分設計とは逆方向の差分解析を可能とした。コンピュータによる機械の制御が、その適用範囲を広げていくに従い、制御ソフトウェアの研究の重要性は増していくものと思われる。このような背景のなかで、ここで提示された手法は、その有効性、独自性の点から高く評価されるものである。

　よって本論文は博士(工学)の学位請求論文として合格と認められる。