| 配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2011年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2010年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2009年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
|
|---|
| 研究概要 |
本研究はシステムやソフトウェアを対象にして,その設計や開発の正当性,妥当性の形式的検証を可能とする計算論理的基盤技術の確立を目的とする.そのための計算論理に基づく方法として,論理プログラムによって対象システムの記述し,プログラム変換技術を用いてその性質を検証するという方法論をとる.次のような3つの研究成果を得た.(1)層状論理プログラムに対する変換において,従来の負の展開規則の条件が誤っていること反例を挙げて示し,これを解決するための新しい負の展開規則を与えた.(2)拡張された負の展開規則を与え,その結果プログラム変換による検証法の適用可能性を拡大させた.(3)余論理プログラ(co-logic programs)に対するプログラム変換規則を与えた.従来知られている検証方法より簡明な検証ができることを示した
|
