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

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

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