Study on Computational Logic-based Methodologies for Building Secure Systems
| Project/Area Number |
21500136
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Intelligent informatics
|
|---|
| Research Institution | Nagoya Institute of Technology |
|---|
Principal Investigator |
SEKI Hirohisa 名古屋工業大学, 大学院・工学研究科, 教授 (90242908)
|
|---|
| Project Period (FY) |
2009 – 2011
|
| Project Status |
Completed (Fiscal Year 2011)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2011: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2010: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2009: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Keywords | 計算論理 / 推論アルゴリズム / システム検証 / プログラム変換 |
|---|
| Research Abstract |
The overall objective of this research project is to construct a computational-logic based methodology for the verification of complex software systems using the transformational verification method ; we use logic programs to represent a given system and a correctness property we want to prove, and then apply to a logic program encoding the system and the property to be verified, a sequence of transformations that preserve the validity of that property. We have obtained the following three main results :
(1) We have shown that negative unfolding for locally stratified programs proposed in the literature is not always correct, and proposed a new negative unfolding rule which guarantees the preservation of the meaning of a given program.(2) We have proposed an extended framework for unfold/fold transformation of stratified programs, including, among others, an extended negative unfolding. It makes the application conditions of the rule more general, thereby making the transformational verification method more applicable.(3) We have proposed a new framework for unfold/fold transformation of co-logic programs, and proved that our transformation system preserves the intended semantics of co-logic programs. We have shown by some examples that our transformational verification method can be used for verifying some properties of Buchi automata in a succinct way
|
Report
(4 results)
Research Products
(13 results)
