Verification of real-time systems based on proving codes

2016 Fiscal Year Final Research Report

• Project/Area Number: 26540026
• Research Category: Grant-in-Aid for Challenging Exploratory Research
• Allocation Type: Multi-year Fund
• Research Field: Software
• Research Institution: Nagoya University
• Principal Investigator: Yuen Shoji 名古屋大学, 情報科学研究科, 教授 (70230612)
• Research Collaborator: LI Guoqiang 上海交通大学, ソフトウェア学院, 准教授
• Project Period (FY): 2014-04-01 – 2017-03-31
• Keywords: 実時間性 / ソフトウェア検証 / 並行プログラム

Outline of Final Research Achievements

We studied verification techniques for real-time concurrent programs. We investigated following topics: (1) Low-leve code proof for RTOS: We gave a proof for priority flag operation for an open-source RTOS kernel, Toppers/SSP, (2) Reachability analysis for Nested Timed Automata: We gave an approximation and an extension. and (3) we gave an operational semantics of Haskell/Yampa on discrete timed runtime environment to show a faulty behavior of hybrid system programs.

Free Research Field

並行計算