|
本研究では、実時間性を持つ並行プログラムに対する証明に基づいた検証技法を与える。以下の３つの観点から研究を実施した。(1) コード証明：オープンソースのToppers RTOSの最小モデルであるSSPカーネルのソースコードに対して分離論理によるコードの証明を行った。ビットマップによる優先度フラグの操作が正しく行われることを示した。(2)実時間プログラムの実行モデルとなるNested Timed Automataのエラー到達可能性検査技法を研究した。(3) 関数型言語のDSLであるYampaに対して離散的に実行する場合の動作意味を与えた。
|
