Verification of real-time reactive systems in high-level programming languages

2016 Fiscal Year Final Research Report

• Project/Area Number: 25280023
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Partial Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Nagoya University
• Principal Investigator: Yuen Shoji 名古屋大学, 情報科学研究科, 教授 (70230612)
• Co-Investigator(Kenkyū-buntansha): 寺内 多智弘 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70447150)
• Research Collaborator: LI Guoqiang 上海交通大学, ソフトウェア学院, 准教授 ; IMAI Keigo 有限会社 : ITプラニング ; Ulidowski Irek レスター大学, 情報学部, 准教授
• Project Period (FY): 2013-04-01 – 2017-03-31
• Keywords: 実時間システム / 到達可能性解析 / プッシュダウンシステム / クロック凍結

Outline of Final Research Achievements

This study presents a safety verification of real-time programs described by a high level programming language with syntax such as recursive calls and interrupt handlings. We proposed a new behavioral model called 'Nested Timed Automata', NeTA for short. The state reachability of NeTA is shown to be decidable. This shows the safety verification is possible. NeTA is a pushdown system whose stack alphabets are timed automata. We also introduced the clock freezing for clocks of timed automata while it is on the stack. It is shown that the reachability is kept decidable under a certain condition. We investigated an efficient Zone-constrcution method to improve the efficiency.

Free Research Field

並行計算モデル