1-4hit |
Izumi MASUBUCHI Tokihisa TSUJI
Stability analysis is one of the most important problems in analysis of hybrid dynamical systems. In this paper, a computational method of Lyapunov functions is proposed for stability analysis of hybrid automata that have set-valued vector fields. For this purpose, a formulation of matrix-valued sums of squares is provided and applied to derive an LMI/LME problem whose solution yields a Lyapunov function.
Yosuke MUTSUDA Takaaki KATO Satoshi YAMANE
We can model embedded systems as hybrid systems. Moreover, they are distributed and real-time systems. Therefore, it is important to specify and verify randomness and soft real-time properties. For the purpose of system verification, we formally define probabilistic linear hybrid automaton and its symbolic reachability analysis method. It can describe uncertainties and soft real-time characteristics.
Izumi MASUBUCHI Seiji YABUKI Tokihisa TSUJI
This paper provides a computational method to construct a Lyapunov function to prove a stability of hybrid automata that can have nonlinear vector fields. Algebraic inequalities and equations are formulated, which are solved via LMI optimization. Numerical examples are presented to illustrate the proposed method.
Jih-Ming FU Trong-Yen LEE Pao-Ann HSIUNG Sao-Jie CHEN
Most of current codesign tools or methodologies only support validation in the form of cosimulation and testing of design alternatives. The results of hardware-software codesign of a distributed system are often not verified, because they are not easily verifiable. In this paper, we propose a new formal coverification approach based on linear hybrid automata, and an algorithm for automatically converting codesign results to the linear hybrid automata framework. Our coverification approach allows automatic verification of real-time constraints such as hard deadlines. Another advantage is that the proposed approach is suitable for verifying distributed systems with arbitrary communication patterns and system architecture. The feasibility of our approach is demonstrated through several application examples. The proposed approach has also been successfully used in verifying deadline violations when there are inter-task communications between tasks with different period lengths.