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

STUDY ONAUTOMATIC VERIFICATION OF HIGHLY RELIABLE SOFTWARE BYINFINITE STATE MODEL CHECKING

高可靠软件无限状态模型检验自动验证研究

基本信息

批准号：
18500023
负责人：
SEKI Hiroyuki
金额：
$ 2.48万
依托单位：
Nara Institute of Science and Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2006
资助国家：
日本
起止时间：
2006 至 2007
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18500023/
关键词：
FORMAL VERIFICATION MODEL CHECKING STATIC ANALYSIS FORMAL LANGUAGE ACCESS CONTROL SECURITY EXECUTION HISTORY XML ソフトウェア学

项目摘要

(1) Model Checking Methods for Recursive Programs: We defined a formal model for programs with access control based on execution history, called HBAC programs and showed that the verification problem for HBAC programs is solvable in polynomial time under a practical assumption. We also proposed a few optimization techniques based on the elimination of useless rules of context-free grammar (CFG). We conducted verifications of two examples, namely, Chinese wall policy and an online banking system, using our implemented verification tool. The verification time for the former problem was 64 seconds when the number of permissions was eighty, and the verification time for the latter problem was 0.01 second when the number of permissions was sixty.(2) Information Flow Analysis: A new information flow analysis method for HBAC programs was proposed. Using the method, we can verify a property of information flow extended to execution paths. Also, we extended a self-composition method so that recursive programs can be analysed.(3) Expressive Power of History-based Access Control: We clarified the relation among the expressive powers of various access control models based on execution history.(4) A Formal Model of Aspect-Oriented Program: A formal model called A-LTS for a pointcut and advice was defined and it was shown that the languages accepted by A-LTSs, deterministic context-free languages (CFLs) and linear CFLs are pairwise incomparable.(5) Other research results.(a) A new class of tree automata called TAN was defined by incorporating a rewrite system modulo equational theory into a standard tree automaton, and discussed the decidability of the fundamental problems of TAN.(b) Computational complexity of the disclosure tree strategy (DTS) in trust negotiation was clarified and an efficient algorithm was also proposed under practical conditions.(c) We proposed a secondary structure prediction method for interacting RNA based on a parsing algorithm for multiple CFG.

(1)递归程序的模型检测方法：我们定义了一个形式化的模型，基于执行历史的访问控制的程序，称为HBAC程序，并表明，验证问题的HBAC程序是在多项式时间内解决的一个实际的假设。在此基础上，提出了一些基于上下文无关文法（CFG）的优化技术。我们进行了验证的两个例子，即中国墙政策和网上银行系统，使用我们实现的验证工具。当权限数为80时，前一个问题的验证时间为64秒，当权限数为60时，后一个问题的验证时间为0.01秒。(2)信息流分析：提出了一种新的HBAC项目信息流分析方法。利用该方法，我们可以验证信息流扩展到执行路径的一个性质。此外，我们扩展了自组合方法，使递归程序可以分析。(3)基于历史的访问控制的表现力：我们阐明了各种基于执行历史的访问控制模型的表现力之间的关系。(4)一个面向A-LTS的程序形式化模型：定义了一个用于切入点和建议的A-LTS形式化模型，并证明了A-LTS所接受的语言、确定性上下文无关语言（CFL）和线性CFL是两两不可比的。(5)其他研究成果。(a)通过将重写系统模方程理论引入到标准树自动机中，定义了一类新的树自动机TAN，并讨论了TAN基本问题的可判定性。(b)阐明了信任协商中披露树策略的计算复杂性，并在实际情况下提出了一种有效的算法。(c)提出了一种基于多重CFG解析算法的相互作用RNA二级结构预测方法。

项目成果

期刊论文数量（0）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Languages Modulo Normalization

语言模归一化

DOI：
发表时间：
2007
期刊：
Lecture Notes in Artificial Intelligence (FroCos07) 4720
影响因子：
0
作者：
Isao Yagi;Yoshiaki Takata and Hiroyuki Seki;中所武司;Hitoshi Ohsaki and Hiroyuki Seki
通讯作者：
Hitoshi Ohsaki and Hiroyuki Seki

A Labeled Transition Model A-LTS for Histroy-based Aspect Weaving and Its Expressive Power

基于历史方面编织的标记转换模型 A-LTS 及其表达能力