講演名 2002/2/25
ハイブリッドシステムの構成的証明とその計算機実験
山根 智,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) ハイブリッドシステムはアナログ環境に組み込まれたデジタルな実時間システムであり,信頼性保証が重要である.信頼性保証を効率的に実現するために,以下のように,我々はハイブリッドシステムの構成的な仕様記述と検証の手法を提案する:(1)ハイブリッドシステムのモジュール単位の仕様を表現するために,フェーズ遷移モジュールを開発する.(2)モジュール単位の計算の実現性を保証するために,フェーズ遷移モジュールのreceptivenessの検証手法を開発する.(3)安全性や活性といった検証性質に直接関係するモジュール部分のみを検証対象とするために,フェーズ遷移モジュールの検証ルールを開発する.
抄録(英) Hybrid systems are digital real-time systems that are embedded in analog environments. It is important to guarantee their qualities. In order to guarantee them, we propose compositional specification and verification methods for hybrid systems as follows: (1)In order to represent a modular specification of hybrid systems, we develop phase transition modules. (2)In order to guarantee feasibilities of modular computations, we propose verification methods of receptiveness. (3) In order to deductively verify safety and liveness properties of only the part related to the properties, we develop verification rules of phase transition modules.
キーワード(和) ハイブリッドシステム / 構成的証明 / 検証 / 仕様記述
キーワード(英) hybrid systems / compositional proof / specification / verification
資料番号 SS2001-49
発行日

研究会情報
研究会 SS
開催期間 2002/2/25(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Software Science (SS)
本文の言語 ENG
タイトル(和) ハイブリッドシステムの構成的証明とその計算機実験
サブタイトル(和)
タイトル(英) Compositional Proof of Hybrid Systems and its experiences
サブタイトル(和)
キーワード(1)(和/英) ハイブリッドシステム / hybrid systems
キーワード(2)(和/英) 構成的証明 / compositional proof
キーワード(3)(和/英) 検証 / specification
キーワード(4)(和/英) 仕様記述 / verification
第 1 著者 氏名(和/英) 山根 智 / Satoshi YAMANE
第 1 著者 所属(和/英) 金沢大学工学情報システム工学科
Faculty of Engineering, Kanazawa University
発表年月日 2002/2/25
資料番号 SS2001-49
巻番号(vol) vol.101
号番号(no) 673
ページ範囲 pp.-
ページ数 8
発行日