| Budget Amount *help |
¥2,200,000 (Direct Cost: ¥2,200,000)
Fiscal Year 2004: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2003: ¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 2002: ¥600,000 (Direct Cost: ¥600,000)
|
|---|
| Research Abstract |
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
|
