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: ¥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.

Research Products

• [Int'l Joint Research] 上海交通大学/復旦大学/華東師範大学(中国)
• [Int'l Joint Research] レスター大学/インペリアル・カレッジ(英国)
• [Int'l Joint Research] 上海交通大学(中国)
• [Int'l Joint Research] インペリアルカレッジ(英国)
• [Journal Article] Compositional Synthesis of Leakage Resilient Programs (2017)
  • Author(s): Arthur Blot, Masaki Yamamoto, and Tachio Terauchi
  • Journal Title: Lecture Notes in Computer Science Volume: 10204 Pages: 277-297
  • DOI: 10.1007/978-3-662-54455-6_13
  • ISBN: 9783662544549, 9783662544556
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] クロック凍結機構を持つ稠密時間プッシュダウンオートマトンの記号実行 (2017)
  • Author(s): 平岡祥、結縁祥治
  • Journal Title: 信学技報,SS2016-60 Volume: 116-512 Pages: 1-6
  • Acknowledgement Compliant
• [Journal Article] Androidアプリケーションの並行実行における予期しない消費電力増加の検出 (2017)
  • Author(s): 稲垣貴大・結縁祥治
  • Journal Title: 信学技報,SS2016-60 Volume: 116-512 Pages: 85-90
  • Acknowledgement Compliant
• [Journal Article] クロック凍結機構を持つ稠密時間プッシュダウンオートマトンのゾーン構成による検証 (2016)
  • Author(s): 平岡祥、結縁祥治
  • Journal Title: 信学技報,SS2016-25 Volume: 116-277 Pages: 43-48
  • Acknowledgement Compliant
• [Journal Article] On Reachability Analysis of Updatable Tiemd Automata with One Updatable Clock (2016)
  • Author(s): Yunqing Wen, Guoqiang Li, Shoji Yuen
  • Journal Title: Lecture Notes in Computer Science Volume: 9559 Pages: 147-161
  • DOI: 10.1007/978-3-319-31220-0_11
  • ISBN: 9783319312194, 9783319312200
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] Temporal Verification of Higher-Order Functional Programs (2016)
  • 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: 10.1145/2837614.2837667
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] Nested Timed Automata with Frozen Clocks (2015)
  • Author(s): Guoqiang Li, Mizuhito Ogawa, Shoji Yuen
  • Journal Title: Lecture Notes in Computer Science Volume: 9268 Pages: 189-205
  • DOI: 10.1007/978-3-319-22975-1_13
  • ISBN: 9783319229744, 9783319229751
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR (2015)
  • Author(s): Tachio Terauchi
  • Journal Title: In Proceedings of the 22nd International Static Analysis Symposium (SAS 2015), Lecture Notes in Computer Science Volume: 9291 Pages: 128-144
  • DOI: 10.1007/978-3-662-48288-9_8
  • ISBN: 9783662482872, 9783662482889
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] An Over-Approximation Forward Analysis for Nested Timed Automata. (2015)
  • Author(s): Yunqing Wen, Guoqiang Li, Shoji Yuen
  • Journal Title: 4th International Workshop on SOFL + MSVL (SOFL+MSVL'14), Lecture Notes in Computer Science Volume: 8979 Pages: 62-80
  • DOI: 10.1007/978-3-319-17404-4_5
  • ISBN: 9783319174037, 9783319174044
  • Peer Reviewed / Acknowledgement Compliant
• [Journal Article] Automatic Termination Verification for Higher-Order Functional Programs (2014)
  • Author(s): Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi
  • Journal Title: Proceedings of ESOP 2014, LNCS Volume: 8410 Pages: 392-411
  • DOI: 10.1007/978-3-642-54833-8_21
  • ISBN: 9783642548321, 9783642548338
  • Peer Reviewed / Acknowledgement Compliant
• [Journal Article] Local temporal reasoning (2014)
  • Author(s): Eric Koskinen, Tachio Terauchi
  • Journal Title: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) Volume: CSL-LICS'14 Pages: 1-10
  • DOI: 10.1145/2603088.2603138
  • Peer Reviewed
• [Journal Article] Concurrency and reversibility (2014)
  • 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: 10.1007/978-3-319-08494-7_1
  • ISBN: 9783319084930, 9783319084947
  • Peer Reviewed
• [Journal Article] 時間制約によるAlloy記述の拡張 (2014)
  • Author(s): 黒板亮太, 結縁祥治
  • Journal Title: 信学技法ソフトウェアサイエンス Volume: 113-448 Pages: 1-6
• [Journal Article] Modelling of Bonding with Processes and Events (2013)
  • Author(s): Iain Phillips, Irek Ulidwoski, Shoji Yuen
  • Journal Title: Lecture Notes in Computer Science Volume: 7948 Pages: 141-154
  • DOI: 10.1007/978-3-642-38986-3_12
  • ISBN: 9783642389856, 9783642389863
  • Peer Reviewed
• [Journal Article] Nested Timed Automata (2013)
  • Author(s): Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen
  • Journal Title: Lecture Notes in Computer Science Volume: 8053 Pages: 168-182
  • DOI: 10.1007/978-3-642-40229-6_12
  • NAID: 110009595806
  • ISBN: 9783642402289, 9783642402296
  • Peer Reviewed
• [Journal Article] 無限小定数と限量子除去法によるハイブリッドシステムの検証に向けて (2013)
  • Author(s): 岩塚卓弥、寺内多智弘、結縁祥治
  • Journal Title: 情報処理学会論文誌(PRO) Volume: 6(3) Pages: 20-32
  • NAID: 110009656444
  • Peer Reviewed
• [Presentation] Towards Reachability Analysis of Dense Timed Pushdown Automata with Frozen Clocks (2017)
  • Author(s): Shoji Yuen
  • Organizer: 46th TRS Meeting
  • Place of Presentation: 篠島、愛知県
  • Year and Date: 2017-02-27
• [Presentation] Session Typed Programming with Poles and Lenses (2017)
  • Author(s): Keigo Imai, Shoji Yuen, Nobuko Yoshida
  • Organizer: Dagstuhl Seminar 17501
  • Place of Presentation: Dagstuhl, ドイツ
  • Year and Date: 2017-01-31
  • Int'l Joint Research
• [Presentation] Automatic Termination Verification for Higher-Order Functional Programs (2014)
  • Author(s): Takya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi
  • Organizer: ESOP 2014
  • Place of Presentation: Grenoble, France
• [Presentation] 時間制約によるAlloy記述の拡張 (2014)
  • Author(s): 黒板亮太, 結縁祥治
  • Organizer: 電子情報通信学会ソフトウェアサイエンス研究会
  • Place of Presentation: 沖縄県那覇市
• [Presentation] Nested Timed Automata (2014)
  • Author(s): Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen
  • Organizer: 第16回プログラミングおよびプログラミング言語ワークショップ
  • Place of Presentation: 熊本県阿蘇
• [Presentation] Modelling of Bonding with Processes and Events (2013)
  • Author(s): Iain Phillips, Irek Ulidwoski, Shoji Yuen
  • Organizer: Reversible Computing 2013
  • Place of Presentation: Victoria, Canada
• [Presentation] Nested Timed Automata (2013)
  • Author(s): Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen
  • Organizer: FORMATS 2013
  • Place of Presentation: Buenos Aires, Argentina