| 内容要旨 | | 近年,需要が飛躍的に増大しつつある交換ソフトウェア開発に対する生産性向上への様々な取り組みの中で,非形式的なユーザ要求をもとに形式的な仕様を作成・検証・保守さえすれば,後のソースプログラムへは機械的に変換できるという仕様を重視した新しいソフトウェア開発パラダイムが適用されている。このパラダイムに則ってSDL,LOTOS,Estelleやペトリネット等の各種の仕様記述言語を用いた開発支援システムが構築されている。ところが,現在各機関で構築されている支援システムはいずれも高級技術者が使用することを前提としており,かつ実用化という点で必ずしも満足できるものにはなっていないのが実情である。つまり,通信システムに関してある程度以上の知識を有していることを前提とし,彼らによる記述や検証に重点を置き過ぎていて,一般ユーザレベルで使えるような自動検証ツールとなっておらず,また通信システムを実際に制御するプログラムの作成についてあまり考慮が払われていないという問題がある。 本論文では,交換ソフトウェア開発支援システムの中でこれまで扱われていなかった3つの分野,つまりユーザ要求の仕様化工程の支援,設計仕様の代数的かつ自動的な検証方式,および設計仕様から最終的に動作するプログラム作成までのインプリメンテーション方式について新たな方式を提案し,それを適用することでトータルなソフトウェア開発の生産性を向上しようとするものである。 ここで提案する,統合化交換ソフトウェア開発支援環境のシステム構成図を図1に示す。 図1に示すように,全体システムは以下の3サブシステムからなる。 ・EXPRESS(EXPeRt system for ESS)自然言語で入力した正常処理に関するサービスをもとに,最終的に完全で誤りのないペトリネット(PN)で表現されたサービス仕様を作成するサブシステム ・ALVER(ALgebraic VERification system)作成されたSDL仕様を検証するにあたり,いったんハイレベルネットに変換し,ペトリネットの解析能力を利用して有界性や活性を代数的かつ自動的に検証するサブシステム ・SDE(Sdl Development Environment)SDLで表現された設計仕様に対して各種の検証を行って誤りを除去し,最終的にC++言語で書かれたプログラムを作成するサブシステム  図1:統合化交換ソフトウェア開発支援環境のシステム構成図 EXPRESSでは,一般ユーザ以上の知識を有するが設計者ほどではない人,例えば通信システム販売の営業者の使用を前提としている。ここで提案するサービス仕様作成支援システムEXPRESSの構成を図2に示す。  図2:EXPRESSの構成 まず,端末の操作とそれに対するシステムの応答という形で表された個々のユーザ要求から,ユーザ要求要素およびサービス要素を経てペトリネットで表す個別サービスグラフ(ISG)に変換する手順を明らかにし,さらに複数個のISGを統合して一つの完全な統合サービスグラフ(TSG)を作成する手順を明確にした。 上記2種類のサービスグラフを作成する際に,ユーザ要求に含まれ得るエラーを自動的に検出するために意味検証,論理検証,およびプロトタイピング検証の3つの方法により検証を行った。意味検証では,通信システムを構成するハードウェアを構造的かつ機能的に知識表現して,操作上のエラーを検出する。論理検証では,作成したTSGが統合したISGをすべて含み,それ以外のサービスを含まないかを自動的に検出する。ISGがちょうどペトリネットでいうTインバリアントに対応するため,ISGを統合して生成されたTSGはTインバリアントによって被覆されることに着目する。すなわち,TSGの接続行列から求められるTインバリアントがISGのそれをすべて含み,かつそれ以外を含んでいないことを調べることで自動的に検証することが可能である。プロトタイピング検証では,本サービス仕様作成支援システムを実装したWSに外付けしたハードウェア装置(端末が接続されたPBX)をプロダクションルールを利用して実際に動作させ,ユーザが想定するようなサービスとなるかを確認する。最後に,このように作成した完全で誤りのないTSGからSDL設計仕様に変換する,ペトリネット(PN)-SDL変換手順を明確にした。 ALVERでは,EXPRESSで最終的に作成されるSDLファイルをもとに,準正常処理や異常処理等を追加して得られる設計仕様をいったんペトリネットに変換し,ペトリネットの表現形式のままで自動的に検証する。代数的仕様検証システムALVERの構成を図3に示す。  図3:ALVERの構成 まずPBXのSDL仕様を端末から見た状態の遷移に着目してハイレベルネットに変換する手順を明確にした。ここでハイレベルネットを使用したのは,通常のペトリネットに比較してトークンに色をつけることで表現能力を高めていることから,システムを簡潔に記述できるからである。変換したペトリネットについて,プレースとトランジションの接続関係を表す接続行列から求められる2つのインバリアントを用いてその構造的な側面から仕様の検証を行う。つまり,Sインバリアントを用いて有界性を調べ,Tインバリアントを用いてデッドロックの検出を行う手法を明確にした。一般に,ハイレベルネットでインバリアントを求めることは容易ではない。しかし,この場合,トークンを無色とした通常のペトリネットとして求めたインバリアントがそのまま使え,有界性や活性について安全側に立った検証を行うことができる。 さらに,通信システムには機能拡張が多いことに鑑みて,インクリメンタルな設計に対処する必要があることに着目した。つまり,機能追加により仕様を追加した部分に誤りが生成されることは十分予想されることとして,その除去のための措置は種々考えられている。しかし,現実に問題となるのは,仕様を追加したことによって,もともと有していた仕様に誤りが混入してしまうことである。これを自動的に検出するため,仕様追加前に成り立っていた有界性や活性といった諸性質を仕様追加後も失っていないことを確認する手順を明確にした。つまり,仕様追加前に求められる両インバリアントが仕様追加後も求められることでそれを検証できる。これはすべて自動的に行えるので極めて有効である。 SDEでは,十分に検証され完全なものとなったSDL設計仕様をもとに,実際にハードウェア装置を制御するプログラムを作成する。まず,実環境の選定についてソフトウェアの移植性と再利用性に留意して,オペレーションシステムとしてTRON仕様OSを,プログラミング言語としてC++言語を採用した。そして,TRON仕様OSの上にSDL/OSを構築し,SDLから変換したC++のプログラムがそのままの形で動くようにした。このSDL/OSは,C++のクラスを利用したライブラリであり,TRON仕様OSの有するタスク管理機能,メッセージ通信機能を利用して,それぞれSDLプロセスの制御,タイマの管理を実行する。なお,このSDL/OSは一つのオペレーティングシステムに対して一度作成すればよいものである。これらの関係を図4に示す。  図4:SDLアプリケーション,SDL/OSおよびTRON仕様OSの間の関係 以上述べてきた開発方式を,実際に伝送装置監視システムとPBX試作システムの2つの試作に適用した。伝送装置監視システムは,特にSDLによらない従来の方式によっても開発を行い,本方式と生産量や生産性等の比較を行った。それによると,設計量は従来方式に比べて約52%に削減された。一般に,プログラムの生産性はプログラミング言語によらず一定で,従って高級言語を使用すればそれだけ生産性が向上するといわれるので,その分生産性が向上すると考えられ,実際の評価でもそれが確認できた。 試作したPBXについて同じハードウェア装置で従来方式で作成したものとの性能比較において,約32%への性能低下の補償として2つの性能向上手法を提案した。一つはSDLプロセスとOSタスクとの対応であり,もう一つはプロセス間通信の実装に関してである。 まず,OSタスクの生成・削除といったオーバヘッドを少なくするために,複数個のプロセスを一つのタスクに対応させることとした。タイマ以外のシグナルを受信することなく動作するプロセスである能動プロセスと,その能動プロセスからシグナルを受信して動作する受動プロセスとを一つのタスクに対応させることで性能低下を防止することとした。プロセス間通信の実装は同期通信の実現方式を考慮したものである。非同期通信を基本とするSDLで,同期通信的な機能を実現させるため,あるプロセスが他のプロセスからのシグナルの到着まで待ち状態にいるときに両プロセスは直列関係にあるとし,それらを一つのタスクに対応させ,かつ通信を関数呼出しで実現することで処理の高速化を図った。以上の2つの性能改善をPBX試作システムに適用し,適用前に比較して性能を56%向上させることができた。 |