Development of design methodologies and support environments of high-reliability embedded systems based on hybrid models

基于混合模型的高可靠性嵌入式系统的设计方法和支持环境的开发

• 批准号: 14580368
• 负责人: YAMANE Satoshi
• 金额: $ 1.41万
• 依托单位: Kanazawa University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2002
• 资助国家: 日本
• 起止时间: 2002 至 2004
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-14580368/
• 关键词: hybrid model; embedded systems; design method for high-reliability; deductive refinement verification; modular deductive verification; model-checking; preemptive scheduler; probabilistic hybrid automaton; 非線形ハイブリッドシステム; 確率ハイブリッドシステム; 到達可能解析; 近似

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 … More 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. Less

显然，混合系统是嵌入模拟环境的数字实时系统，对于嵌入式系统来说，开发高可靠性嵌入式系统的设计方法也很重要。在本文中，我们提出了演绎精化理论、演绎模验证理论、从控制理论到混合自动机的转换方法、基于证明理论和模型检验的概率混合自动机的符号验证方法。研究以下内容：（1）我们通过从规范的内部行为到实现的行为的细化映射提出了细化公理。我们使用PVS实现了细化公理，并证明了其有效性。（2）我们提出了混合系统的模块化规范和验证方法。如下：（a）为了表示混合系统的模块化规范，我们开发了相变模块。（b）为了保证模块化计算的可行性，我们提出了验证方法(c)为了演绎地验证仅与属性相关的部分的安全性和活性属性，​​我们开发了相变模块的验证规则。(3)我们正式指定实时软件并验证是否是实时操作系统相对于使用混合自动机的细化验证方法的规范是有效的。此外，我们使用调度理论验证了可调度性，我们可以统一指定实时软件并验证其有效性。即时的软件，它由周期进程和一个CPU上的固定优先级抢占式调度策略组成。(4)我们提出正式的开发方法如下：(a)首先，我们使用Matrix_x和混合自动机分层指定混合系统。(b)接下来，我们通过将 Matrix_x 转换为混合自动机，将混合系统构建为混合自动机的并行组合。(c)最后，通过将混合自动机近似为线性混合自动机，我们验证了混合系统是否(5)提出了概率线性混合自动机及其符号可达性分析方法，并基于Mathematica实现了验证器，并证明了其有效性。

项目成果

ハイブリッドシステムのモジュールの仕様記述と検証の手法

混合系统模块规格说明及验证方法

• 发表时间: 2003
• 期刊: 情報処理学会論文誌 Vol.44, No.3
• 作者: 山根 智

山根 智: "Formal development methodology of hybrid systems"IKE'02. 10. 469-475 (2002)

Satoshi Yamane：“混合系统的正式开发方法”IKE02。 10. 469-475 (2002)。

Satoshi Yamane: "Formal refinement verification method of real-time systems with discrete probability distributions"2nd International Workshop on Automatic Verification of Infinite-State Systems. 2. 202-215 (2003)

Satoshi Yamane：“具有离散概率分布的实时系统的形式化细化验证方法”第二届无限状态系统自动验证国际研讨会。

Satoshi Yamane: "Deductive Verification of Probabilistic Real-Time Systems"Proceeding of IEEEThird International Workshop on Assurance in Distributed Systems and Networks. 3. 33-37 (2004)

Satoshi Yamane：“概率实时系统的演绎验证”IEEE 第三届分布式系统和网络保证国际研讨会论文集。

Satoshi Yamane: "Deductive Schedulability Verification Methodology of Real-Time Software using both Refinement Verification and Hybrid Automata"Porceedings of IEEE 27th COMPSAC. 27. 527-533 (2003)

Satoshi Yamane：“使用细化验证和混合自动机的实时软件的演绎可调度性验证方法”IEEE 第 27 届 COMPSAC 会议记录。