Execution Time Analysis for Binary Code Executed on a Pipelined Processor Using Parametric Model Checking

• Item type: Trans(1)
• 公開日: 2006-10-15
• タイトル: Execution Time Analysis for Binary Code Executed on a Pipelined Processor Using Parametric Model Checking
• タイトル / 言語: en
• タイトル: Execution Time Analysis for Binary Code Executed on a Pipelined Processor Using Parametric Model Checking
• 言語: eng
• キーワード / 主題Scheme: Other
• キーワード / 主題: 発表概要
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: Department of Information Networking Graduate School of Information Science and Technology Osaka University
• 著者所属: Department of Information Networking Graduate School of Information Science and Technology Osaka University
• 著者所属: Department of Information Networking Graduate School of Information Science and Technology Osaka University
• 著者所属: Department of Information Networking Graduate School of Information Science and Technology Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Information Networking, Graduate School of Information Science and Technology, Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Information Networking, Graduate School of Information Science and Technology, Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Information Networking, Graduate School of Information Science and Technology, Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Information Networking, Graduate School of Information Science and Technology, Osaka University
• 著者名: Hirohisa, Fujita; Shiro, Fukamati; Akio, Nakata; Teruo, Higashino
• 著者名(英): Hirohisa, Fujita; Shiro, Fukamati; Akio, Nakata; Teruo, Higashino
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: Execution time estimation of programs is important in designing real-time embedded systems. However it is a difficult task since a processor architecture becomes complicated with cache memory pipeline or other features. In this presentation we propose a method to analyze execution time of a sequential program running on a simple pipelined processor. The proposed method requires three inputs: an analysis target program a specification of instruction cache and pipeline architecture of the execution environment of the given program and a relation (required property) among the worst/best case execution times (WCET/BCET) of some code blocks of the given program written in a linear inequality. The output of the analysis is the condition in order that the given program satisfies the required property when executed by the processor having specified architecture. The derived condition contains the number of iterations for each loop and the CPU clock frequency as the parameters. In the proposed method we use the analysis technique parametric model checking for a subclass of Parametric Timed Automata called Parametric Time-Interval Automata (PTIA). We propose an algorithm to generate a PTIA representing the execution of the given program and the given execution environment. Since each transition condition of PTIA is restricted to the form of the interval we can derive such a relation as efficient as the traditional nonparametric model checking. We have applied the proposed analysis method to a simple real-time software and successfully derived the parameter condition in order to satisfy a given required property.
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Execution time estimation of programs is important in designing real-time embedded systems. However it is a difficult task since a processor architecture becomes complicated with cache memory, pipeline or other features. In this presentation,we propose a method to analyze execution time of a sequential program running on a simple pipelined processor. The proposed method requires three inputs: an analysis target program, a specification of instruction cache and pipeline architecture of the execution environment of the given program, and a relation (required property) among the worst/best case execution times (WCET/BCET) of some code blocks of the given program, written in a linear inequality. The output of the analysis is the condition in order that the given program satisfies the required property when executed by the processor having specified architecture. The derived condition contains the number of iterations for each loop and the CPU clock frequency as the parameters. In the proposed method, we use the analysis technique, parametric model checking, for a subclass of Parametric Timed Automata called Parametric Time-Interval Automata (PTIA). We propose an algorithm to generate a PTIA representing the execution of the given program and the given execution environment. Since each transition condition of PTIA is restricted to the form of the interval, we can derive such a relation as efficient as the traditional nonparametric model checking. We have applied the proposed analysis method to a simple real-time software and successfully derived the parameter condition in order to satisfy a given required property.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 47, 号 SIG16(PRO31), p. 95-95, 発行日 2006-10-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会