Yoshio HARADA
通信サービス設計および検証における
形式的支援に関する研究
Abstract:近年，電気通信分野での著しい技術革新の進展と通信サービスの普及に伴い，通信
サービスに対する利用者の要求が多様化・高度化している．このような需要に対し
て，迅速な新規サービス開発と提供が必要となり，通信ソフトウェアの効率的かつ迅
速な開発技術の確立が早急の課題となっている．通信サービス設計においては，新規
サービス単独の動作仕様を規定するだけでなく，新規サービス仕様と既存サービス仕
様との相互作用（サービスインタラクション）を解析し，サービス仕様間に生じる矛
盾を解消し，サービス全体として矛盾のない仕様を作成する必要がある．ところが，
一般に，相互作用の数は，既存サービス数が増えると組合せ的に増大し，その相互作
用に隠れたサービス仕様矛盾の検証は，人手で行う事のできる範囲を越えた作業と
なっている．相互作用解消の問題は，1991年12月，CCITTによってインテ
リジェントネットワークのための技術的勧告として提示されたCS1(IN Capability
Set 1)においても，今後の重要な課題のひとつに挙げられている．
サービス相互作用解析を機械的に支援するためには，まず，サービス仕様を形式的
に記述する必要がある．そのため，通信サービス仕様として利用者の観点から見える
動作を対象とし，サービス動作を形式的な規則形式により記述する手法(STR：
State Transition Rule)を提案している．また，STR手法を用いて通信サービスは記
述されていることを前提とし，新規サービスと既存サービスからサービス合成動作を
作成し，そのサービス合成動作を基盤に相互作用に含まれる矛盾検出支援方式を提案
している．
本論文では筆者がこれまでに行ってきた，通信サービス設計および検証における形
式的支援に関する以下の研究項目について述べる．
①通信サービス記述方式
②通信サービス設計支援方式
③通信サービス競合（非決定性）検出方式
④通信サービス相互作用に含まれる意味的矛盾動作検出支援方式
⑤通信サービス課金仕様競合検出方式