形式言語理論に基づく通信制御プログラムの処理系列検証方法

概要

論文の詳細を見る
プログラムにおける各種資源アクセス処理は,資源の確保→情報の設定→情報の参照→資源の解放,というような一定の順序に従って実行されねばならない.形式言語理論によれば,このような実行順序規則の多くは正規文法で表すことができ,このとき同規則に基づく資源アクセス処理系列の集合は正規言語となることから,処理系列の実行順序規則性の検証は文の帰属問題に帰着できる.一方,正規言語は有限オートマトンと等価である.本論文ではこの点に着目し,通信制御プログラムを対象に,ソースプログラムのパス解析によりその通過し得る径路を網羅的に抽出し,各径路中の資源アクセス処理系列がその実行順序規則に基づく正規言語と等価なオートマトンに受理されることを確認することにより,タイマ,バッファ等の資源アクセス処理の実行順序の妥当性を検証する方法を提案する.本検証方法は次の特徴を有する:(1)ループ系列については,ループ部分を正規表現で表すとともに非ループ系列と合成することにより,実際のループ回数に依存しない検証が可能である.(2)同一資源に対するアクセス処理が複数のモジュールで実行される場合にも,モジュール間インタフェース情報の解析により検証可能である.また,上記方法に基づく検証システムの試作例についても述べる.本検証方法および検証システムの適用により,プログラムの信頼性・生産性向上が期待できる.
一般社団法人情報処理学会の論文
1993-01-15

著者

山下博之
NTT 情報通信研究所

形式言語理論に基づく通信制御プログラムの処理系列検証方法

スポンサーリンク

概要

著者

関連論文

スポンサーリンク