학술논문
Modeling, Specification and Model Checking of Dynamically Reconfigurable Processors / 動的再構成可能プロセッサのモデル化，仕様記述とモデル検査
Document Type
Journal Article
Author
Source
コンピュータ ソフトウェア / Computer Software. 2011, 28(1):1-190
Subject
Language
Japanese
ISSN
0289-6540
Abstract
In this paper, we propose formal verification for cooperated systems consisting of CPU and DRP. First, we specify CPU as real-time systems and DRP as hybrid systems using hybrid automata. Next, we verify schedulability using model cheking. In order to avoid state explosions, we separate schedulability verifications into the following two verifications.1. We verify whether parallel composition of CPU automaton and worst DRP is schedulable or not.2. We verify whether parallel composition of DRP automaton and worst CPU is schedulable or not.We have realized schedulability verification of CPU and DRP by the above two verifications.