Hybrid Automata Theoretic Specification and Verification of CPU-DRP Embedded Systems

Abstract

In this paper, we propose formal modeling, specifi- cation and verification for CPU-DRP systems based on hybrid automata. First, we specify CPU and environment as real- time systems, and specify DRP as hybrid systems by using hybrid automata. Next, we verify various properties by model checking using HYTECH. We have realized verification of parallel composition of CPU, DRP and environment.