STUDY ONAUTOMATIC VERIFICATION OF HIGHLY RELIABLE SOFTWARE BYINFINITE STATE MODEL CHECKING

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

(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.