权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Study on Computational Logic-based Methodologies for Building Secure Systems

基于计算逻辑的安全系统构建方法研究

基本信息

批准号：
21500136
负责人：
SEKI Hirohisa
金额：
$ 2.66万
依托单位：
Nagoya Institute of Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2009
资助国家：
日本
起止时间：
2009 至 2011
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-21500136/
关键词：
計算論理推論アルゴリズムシステム検証プログラム変換

项目摘要

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

本研究计画的总体目标是建构一套以计算逻辑为基础的方法论，以转换式验证法来验证复杂的软体系统;我们使用逻辑程序来表示给定的系统和我们想要证明的正确性属性，然后应用于对系统和要验证的属性进行编码的逻辑程序，保持该属性有效性的一系列变换。我们得到了以下三个主要结果：（1）证明了文献中提出的局部分层规划的负开折并不总是正确的，并提出了一个新的负开折规则，该规则保证了给定规划的意义保持。(2)我们已经提出了一个扩展的框架展开/折叠变换的分层程序，包括，除其他外，一个扩展的负展开。它使规则的适用条件更一般化，从而使转换验证方法更具有适用性。(3)我们提出了一个新的框架展开/折叠转换的协同逻辑程序，并证明了我们的转换系统保持预期的语义协同逻辑程序。通过一些例子表明，我们的变换验证方法可以简洁地用于验证Buchi自动机的一些性质