Verification of real-time systems based on proving codes
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
|
Project Status |
Completed (Fiscal Year 2016)
|
Budget Amount *help |
¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
Fiscal Year 2016: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2015: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2014: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
Keywords | 実時間性 / ソフトウェア検証 / 並行プログラム / 実時間プログラム / 関数型言語 / ハイブリッドシステム / プログラミング言語 / 実時間処理 / コード証明 / 分離論理 / 実時間性検証 / スーパーバイザ制御 / Nested Timed Automaton |
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.
|
Report
(4 results)
Research Products
(15 results)