情報社会の発展に伴って情報通信は高度化・多様化の一途をたどっており,電話網による音声主体の通信からインターネットによるマルチメディア情報通信に大きく変遷しようとしている.このような情報通信の実現の核となる通信ソフトウェアの開発量・保守量は増大する一方である.その結果,通信ソフトウェアの開発・保守における作業の効率化と品質の向上が一層重要な課題となってきた.この課題の解決には,開発・保守の初期の段階で作成する(要求)仕様がその後の全作業工程の基本となりまた要となるので,正確な仕様の作成を支援する仕様検証技術が特に重要である.

　これまで仕様検証技術については様々な研究開発が進められてきたが,通信ソフトウェアに適した仕様検証技術についての研究開発は十分ではなかった.

　通信ソフトウェアの中で重要な位置を占めるものの一つに通信プロトコルがある.一般に,通信プロトコルの仕様は大規模で複雑であり,誤りを含むことが少なくなく,その結果通信システムの動作に重大な支障を来たすことがある.従って,プロトコル仕様に含まれる誤りを検出するプロトコル検証は必須である.しかし,これまでに開発されてきたプロトコル検証技術では,検証処理の効率が低く,プロトコル規模が大きくなると検証に必要なメモリ量や処理量が指数関数的に急激に増大するため,多くの実用的規模のプロトコルが検証できないという問題があった.

　通信ソフトウェア仕様の検証には,プロトコル検証だけでは十分ではない.しかし,これまでのところ総合的かつ体系的な検討は少なく,通信ソフトウェア仕様の特徴を考慮した効率的な仕様検証技術は未だ確立されてはいない.例えば,通信ソフトウェア仕様は一般に規模が大きく,通常一部分づつ段階的に作成されるが,このような仕様の段階的作成を効率よく支援する検証技術はほとんど開発されてこなかった.また,通信ソフトウェア仕様の検証はある程度人手による必要があるが,人手による検証を効率よく支援する技術の研究も十分には取り組まれてこなかった.

　このように通信ソフトウェア仕様の検証に関しては,プロトコル検証の効率を大幅に向上できる技術,及び,通信ソフトウェア仕様向きの検証機能を持った新しい効率よい技術の開拓が大きな課題であった.本論文の目的は,これらの課題の解決を図ることにあり,具体的には,次の通り,二つに大別できる.

　本論文の第1の目的は,信号送受信の過不足やデッドロック等,通信ソフトウェア仕様の要となるプロトコルの動作仕様に関する論理的な誤りを検出するプロトコル検証の効率を大幅に向上し,これまでは不可能であった実用的規模のプロトコルの検証を可能とする技術を確立することにある.すなわち,これまでの検証法においてボトルネックとなっていた所要メモリ量と処理量の大幅な削減を可能にする技術の開拓を目標とした.

　本論文の第2の目的は,原始要求に対する通信ソフトウェア仕様の充足性に関する検証を効率よく実現する新しい技術の開拓にある.特に,不完全な仕様の段階的な機能検証を可能にする技術の開拓を目標とした.また,与えられた仕様をできる限り簡明な表現に自動的に変換して検証を容易にすることによって,人手による検証の効率を向上する技術の開拓を目標とした.更に,機能に関する要求条件を入力し,与えられた仕様がそれを満たしているか否かを効率よく検査できる技術の開拓を目標とした.

　本論文では,第1の目的を達成するため,以下に示す4手法を考案し技術開発した.

　本論文は「通信ソフトウェア仕様検証の技術の効率向上に関する研究」と題し、近年極めて多様に展開され、急速に進展している通信用ソフトウェアについて、その検証を高能率化する方法について論じたものであって、全6章よりなる。

　第1章は「序論」であって研究の背景と目的を述べている。通信ソフトウェアの中で重要な位置を占める通信プロトコル仕様に含まれる誤りを検出するプロトコル検証の高能率化と通信ソフトウェア仕様が段階的に作成されるために発生する不完全性を軽減する支援手法の重要性を述べている。

　第2章は「研究の位置づけ」と題し、この分野における従来の研究を総括すると共に、本論文の立場を述べている。通信ソフトウェアの検証の目的ではモデル化が必要であり、本論文としては拡張された有限状態機械モデルを採用し、仕様の記述にはSDL(Specification and Description Language)を使用するものとしている。さらに従来の通信プロトコルの論理検証技術と通信ソフトウェア仕様の意味検証技術について検討し、効率の良い技術が必要であることを述べている。

　第3章は「通信ソフトウェア仕様の検証」と題し、通信ソフトウェアの生産性の品質の向上を図ることを目的として、その初期の段階で作成する仕様に含まれる誤りを検証する技術について、検討している。また、仕様誤りと呼ばれ、誤りの定義を明確化すると共に、仕様検証技術全体を体系的に整理し、仕様検証技術の全体像を明らかにしている。さらに、通信ソフトウェアのライフサイクルについて論じ、機能の追加や変更が絶え間なく要求されるシステムをモデル化している。仕様要件の内、一義性、正当性、一貫性および完全性を劣化させる要因をすべて仕様誤りと定義し、一貫性および完全性を劣化させる誤りを論理誤り、正当性を劣化させる誤りを意味誤りと呼び、それぞれの誤りがないことを検証することを論理検証、意味検証と定義している。

　第4章は「通信プロトコル仕様の論理検証」と題し、プロトコル検証の効率を向上する新しい手法を提案し、評価している。まず通信プロトコル仕様を2個以上のプロセスでモデル化している。このモデルに基づいて、信号定義の過剰、信号定義の不足、デッドロックの3種類の誤りをすべて検出することをプロトコル検証問題と定義している。こうして定義されるプロトコルは実用システムでは膨大な規模のモデルとなり、効率的な検証が困難になる。これに対して本章では、信号を送受信する相手プロセスが1個に限定されるプロセスを削除して検証するプロセス削減法を提案し、プロセス1個を削減することによって検証処理量を1/3〜1/5に減少できることを示している。さらにプロセス状態遷移の一括処理法、プロセス状態遷移図のアサイクリック展開法、段階的プロトコル検証法を提案し、これらを組合わせて適用することによって数百分の1への検証処理量の削減ができることを示している。

　第5章は「通信ソフトウェア仕様の意味検証」と題し、プロトコル記述の正当性を検証する方法について論じている。まず不完全な仕様を段階的に意味検証する方法としてプロトタイピングを提案し、それを実証的に評価している。しかし通信ソフトウェア仕様の意味検証を完全に、機械的に実施することは不可能であり、人手による検証が必要になる。そこで人手による検証の効率を向上させる方法として、与えられた仕様を意味や機能は変更せずより簡明な表現に変換する簡明化処理について提案している。形式簡明化としてはSDLによる表現を標準化して統一的に記述することを提案している。意味簡明化としては簡明なSDL構文をとることなどを提案し、そのための具体的方法を示している。これらによりSDLによる表現を25%程度削減できることを示している。さらに実行系列の検査による意味検証法によって原始要求の充足性を判定する方法を提案し、従来の人手による方法に比べ最大数十分の1以下に検証時間を短縮できるとしている。

　第6章は本論文の結論であり全体の成果をとりまとめている。

　以上のように本研究では通信プロトコルの論理検証および意味検証についてその効率を大幅に向上する方法を提案し、実証したものであって、今後ますます重要になる通信ソフトウェアの開発を効率化する技術を確立しており、電子情報工学に寄与するところが少なくない。よって本論文は博士(工学)の学位論文として合格と認められる。