Verification of real-time reactive systems in high-level programming languages
| 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
|
| Project Status |
Completed (Fiscal Year 2016)
|
| Budget Amount *help |
¥16,770,000 (Direct Cost: ¥12,900,000、Indirect Cost: ¥3,870,000)
Fiscal Year 2016: ¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000)
Fiscal Year 2015: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Fiscal Year 2014: ¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000)
Fiscal Year 2013: ¥6,370,000 (Direct Cost: ¥4,900,000、Indirect Cost: ¥1,470,000)
|
|---|
| 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.
|
Report
(5 results)
Research Products
(27 results)
-
-
-
-
-
-
-
-
-
-
[Journal Article] Temporal Verification of Higher-Order Functional Programs2016
Author(s)
Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno
-
Journal Title
In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), ACM SIGPLAN Notices
Volume: 51 (1)
Pages: 57-68
DOI
Related Report
Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
-
-
-
-
-
-
[Journal Article] Concurrency and reversibility2014
Author(s)
Irek Ulidowski, Iain Phillips and Shoji Yuen
-
Journal Title
Reversible Computation 2014, Lecture Notes in Computer Science
Volume: 8507
Pages: 1-14
DOI
ISBN
9783319084930, 9783319084947
Related Report
Peer Reviewed
-
-
-
[Journal Article] Nested Timed Automata2013
Author(s)
Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen
-
Journal Title
Lecture Notes in Computer Science
Volume: 8053
Pages: 168-182
DOI
NAID
ISBN
9783642402289, 9783642402296
Related Report
Peer Reviewed
-
-
-
-
-
-
-
-
