Parametric Verification towards Design of Real-Time Systems

概要

論文の詳細を見る
Timing characteristic is an important point of concern in the design of real-time systems, because the systems are to operates under time-critical conditions. In recent years, verification techniques for reasoning about timed systems have been developed. Those techniques require detailed information about specific timing of a system. In this research, we develop a verification-driven approach for improving the correctness in the design of real-time systems. Our technique abstracts the detailed of timing information of the system by using time parameters. We propose parametric timed structure and parametric temporal logic P_<AR>CTL for describing real-time systems behavior and specifying timing properties with time parameters. As for the verification, we develop a model checking algorithm whose results are specific constraints over time parameters which can beused as guidelines for improving the design of the system.
社団法人電子情報通信学会の論文
2005-10-07