OSIセション層の代数的仕様記述から

点击翻译按钮获取中文摘要

1.自然語(英語)と状態遷移表で記述されたOSIセション層の規格を代数的仕様記述言語ASLを用いて記述した。まず、セションプロトコル仕様のうち、カーネル、,半二重、全二重、小同期、大同期機能単位に関する部分を記述し、次いで再同期機能単位の部分を追加した。これにより代数的仕様記述法について次のような知見を得た。(A)記述の追加・変更が容易であること。(B)代数的仕様に用いている関数名や述語名には、原仕様で用いられているものを利用しているなど元の規格で用いられている概念をよく反映し、しかも形式的意味が容易に理解できること。(C)理解の容易性が高いこと。なお、記述の規模は公理の個数で826であり、再同期機能単位の追加の過程での検証により、それまでの記述の誤りと再同期機能単位の記述の誤りがそれぞれ4個ずつ発見された。2.代数的に記述されたプロトコルを通信プログラムに変換する方法について検討し、本研究で扱う変換の問題を代数的仕様の詳細化の問題として形式的に定義した。さらに、抽象的順序機械の形で記述されたプロトコルの代数的仕様をC言語で記述されたプログラムに変換するコンパイラを設計・試作し、セションプロトコルの代数的仕様のうちセションプロトコルマシン(SPM)の動作に関する部分をこのコンパイラを用いて変換した。コンパイルに要した時間は、IBMのワークステーション6150上のUNIX環境下で、CPU時間49.6秒(内訳は構文解析:47.3秒、目的プログラム生成:2.3秒)であった。3.上位層、下位層および相手SPMを模倣するテスト環境を作成し、ローカルテスト方式により、17個のテスト系列(平均の系列長は、8.4)について、目的プログラムが正しく動作することを確認した。なお、これらのテスト系列には、INTAP試験検証システムのTest suites中の該当するすべてのテスト系列が含まれている。