| 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)
|
|---|
| 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.
|
