振る舞い仕様の効率的な実現可能性判定のための分割検証法

高效确定行为规范可行性的分割验证方法

• 批准号: 22K11980
• 负责人: 島川 昌也
• 金额: $ 2.08万
• 依托单位: Takushoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2022
• 资助国家: 日本
• 起止时间: 2022-04-01 至 2025-03-31
• 项目状态: 未结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22K11980/
• 关键词: 仕様検証; 実現可能性; ω-オートマトン

時間論理などでシステムの振る舞いに関する仕様を厳密に記述し，それを検証する形式仕様検証は，人力では見つけにくい欠陥を計算機によって自動で検出できるが，計算コストが高いという問題がある．本研究では，特に計算コストが高いリアクティブシステム仕様の実現可能性判定の効率化を目的として，分割検証法について検討する．ここで検討する分割検証の枠組みは次のとおりである：(1)仕様をいくつかのサブモジュールに分割，(2)各サブモジュール仕様について，それと等価なωオートマトンを構成，(3)各サブモジュール仕様のオートマトンに簡約などを適用，(4)各サブモジュール仕様のオートマトンを統合，(5)統合したオートマトンを分析．このような分割検証では，ステップ3の簡約方法が全体としての効率を大きく左右する．本研究では，そこへ新たなアイディアを導入する．既存研究では，単なるオートマトンの最小化（等価な変換）しか行われていなかったが，本研究では，統合後の検証で不必要な局所的な情報の除去（意味的にも異なる変換）も行う．2022年度は，サブモジュール仕様のオートマトンの簡約において，局所的な「応答イベント」の情報を除去する分割検証を提案した（リアクティブシステム仕様は要求イベントと応答イベントの生起タイミングを規定するものである）．そして，その正当性，つまり，提案した方法では局所的な応答イベント情報の除去を行っても正しく実現可能性の判定が行えること（除去しないときと同様の判定結果が得られること）を証明した．

形式化规范验证使用时间逻辑严格描述有关系统行为的规范并对其进行验证，允许计算机自动检测人工难以发现的缺陷，但存在计算成本较高的问题。在本研究中，我们研究了一种分割验证方法，旨在提高确定反应式系统规范可行性的效率，因为反应式系统规范的计算成本特别高。这里考虑的分割验证的框架如下：（1）将规范划分为多个子模块，（2）为每个子模块规范构造一个等效的ω自动机，（3）对每个子模块规范应用约简等。自动机，（4）集成每个子模块规范的自动机，（5）分析集成的自动机。在这种分割验证中，步骤3中的简化方法对整体效率影响很大。在这项研究中，我们引入了一个新想法。现有研究中仅进行了简单的自动机最小化（等效变换），但本研究在集成后验证过程中也去除了不必要的局部信息（语义不同的变换）。 2022年，我们提出了分割验证，以在子模块规范的自动机简化中删除本地“响应事件”信息（反应式系统规范指定请求事件和响应事件发生的时间）。我们还证明了其有效性，即即使去除本地响应事件信息，该方法也能正确判断可行性（与不去除时的判断结果相同）．．

项目成果

A Characterization on Necessary Conditions of Realizability for Reactive System Specifications

反应式系统规范可实现性必要条件的表征

• DOI: 10.1587/transinf.2021fop0005
• 发表时间: 2022
• 影响因子: 0.7
• 作者: TOMITA Takashi;HAGIHARA Shigeki;SHIMAKAWA Masaya;YONEZAKI Naoki
• 通讯作者: YONEZAKI Naoki