ハイブリッドモデルによる組込みシステムの高信頼性設計方法論の構築と支援環境の開発

• Material Type: 文書・図像類
• Title: ハイブリッドモデルによる組込みシステムの高信頼性設計方法論の構築と支援環境の開発
• Author/Editor: 山根, 智; Yamane, Satoshi
• Author Heading: 山根, 智; Yamane, Satoshi
• Publication, Distribution, etc.: 金沢大学 理工研究域電子情報通信学系
• Publication Date: 2005-03
• Publication Date (W3CDTF): 2005-03
• Alternative Title: Development of design methodologies and support environments of high-reliability embedded systems based on hybrid models
• Periodical title: 平成16(2004)年度 科学研究費補助金 基盤研究(C) 研究成果報告書 = 2004 Fiscal Year Final Research Report
• No. or year of volume/issue: 2002-2004
• Volume: 2002-2004
• Pages: 182p.-
• Text Language Code: jpn
• Subject Heading: ハイブリッドモデル; 組込みシステム; 高信頼性設計方法; 演繹的詳細化検証; モジュール演繹的検証; モデル検査; プリエンプティブスケジューラ; 確率ハイブリッドオートマトン; hybrid model; embedded systems; design method for high-reliability; deductive refinement verification; modular deductive verification; model-checking; preemptive scheduler; probabilistic hybrid automaton
• Target Audience: 一般
• Note (General): 組込み型システムはアナログ環境に組み込まれたデジタルな実時間システムであり、ハイブリッドシステム(いわゆる、アナログ動作とデジタル動作が混在するシステム)と考えることができて、信頼性が保証できる設計方法論の構築が要望されている分野である。従来の研究では、詳細化検証、モジュール化、既存手法との連携などの点が考慮されていない。本研究では、詳細化検証、既存の開発手法との連携、確率の導入によるモデルの構築などに着目して、定理証明技術や自動検証技術を駆使しながら、信頼性が保証できる設計方法論の構築を行った。具体的には、本研究では、以下の研究成果をあげた。(1)ハイブリッドシステムの段階的詳細化開発を可能とするために、詳細化写像を用いた、演繹的な詳細化検証理論を開発して、実験的に有効性を実証した。(2)ハイブリッドシステムのモジュール毎の仕様記述と検証の手法を可能とするために、フェーズ遷移モジュールとそのモジュール的演繹検証、receptivenessの演繹的検証を実現して、Stepを用いて、実験的に有効性を実証した。(3)ハイブリッドシステムの重要な事例として、プリエンプティブスケジューラがある。プリエンプティブスケジューラを含む、リアルタイムソフトウェアをハイブリッドシステムとしてモデル化して、仕様記述する手法とそのスケジューラビリティ検証する手法を開発した。事例を用いて、実験的に有効性を実証した。(4)既存のハイブリッドシステムの開発では、制御理論に基づく制御仕様が使われている。制御仕様からハイブリッドモデルへの変換を含む、統合的な開発手法を開発して、現実的な事例により、実験的に有効性を実証した。(5)ハイブリッドシステムのランダム性やソフトリアルタイム性を扱うために、確率の概念を導入して、確率線形ハイブリッドオートマトンを開発して、その記号的な検証理論を開発した。; Hybrid systems are digital real-time systems that are embedded in analog environments. Obviously, correctness is of vital importance for embedded systems. It is important too develop design methodologies far high-reability embedded systems. In existing studies, refinement theories and modular methods have not been studied. In this paper, we propose deductive refinement theories, deductive modular verification theories, transformation methods from control theories to hybrid automata, symbolic verification methods of probabilistic hybrid automata based on proof theories and model-checking. In this paper, we have studied the followings :(1)We propose refinement axioms by a refinement mapping from internal behaviors of specification to behaviors of implementation. We have implemented refinement axioms using PVS, and have demonstrated its effectiveness.(2)We propose modular specifcation and verification method for hybrid systems as follows :(a)In order to represent a modular specification o f hybrid systems, we develope phase transition modules.(b)In order to guarantee feasibilities of modular computations, we propose verification methods of receptiveness.(c)In order to deductively verify safety and liveness properties of only the part related to the properties, we develope verification rules of phase transition modules.(3)We formally specify real-time software and verify whether real-time operating system is valid relative to specification using refinement verification methods of hybrid automata. Moreover, we verify schedulability using scheduling theory. Using our proposed methods, we can uniformally specify real-time software and verify its validity. Finally, we show our proposed methods effective by the real-time software, which consists of periodic processes and a fixed-priority preemptive scheduling policy on one CPU.(4)We propose our formal development method as follows :(a)First, we hierarchically specify hybrid systems using Matrix_x and hybrid automata.(b)Next, we construct hybrid systems as parallel compositions of hybrid automata by transforming Matrix_x into hybrid automata.(c)Finally, by approximating hybrid automata into linear hybrid automata, we verify whether hybrid systems are valid or not using model-checking.(5)We propose probabilistic linear hybrid automaton and its symbolic reachability analysis method. We implement our verilier based on Mathematica, and demonstrate its effectiveness.; 研究課題/領域番号:14580368, 研究期間(年度):2002-2004; 出典：「ハイブリッドモデルによる組込みシステムの高信頼性設計方法論の構築と支援環境の開発」研究成果報告書 課題番号14580368 (KAKEN：科学研究費助成事業データベース（国立情報学研究所）) 本文データは著者版報告書より作成
• DOI: 10.24517/00053965
• Source: https://kanazawa-u.repo.nii.ac.jp/?action=repository_action_common_download&item_id=47641&item_no=1&attribute_id=26&file_no=1
• Access Restrictions: 限定公開
• Rights (production): CC BY-NC-ND
• Related Material: https://kaken.nii.ac.jp/search/?qm=70263506; https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-14580368/; https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-14580368/145803682004kenkyu_seika_hokoku_gaiyo/
• Data Provider (Database): 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）; https://irdb.nii.ac.jp
• Original Data Provider (Database): 金沢大学 : 金沢大学学術情報リポジトリKURA