程序求精新策略及自动验证方法研究

传统的程序求精策略无法求精至可执行程序,且存在验证的可信度低和自动化程度不高的问题。针对上述问题,提出一种较完整的程序求精策略并给出自动验证方法。使用递归定义函数技术刻画问题规约,基于Morgan精化规则程序求精至IMP程序,并使用验证条件生成器(verification condition generator,VCG)自动生成验证条件,通过Isabelle定理证明器验证IMP程序的正确性,最后利用开发平台自动生成C++可执行程序。以最长标志基因序列问题为实例进行程序求精和自动验证,检验了所提策略的有效性。该策略提高了算法程序开发的正确性,减轻了传统验证烦琐的工作量。

基于多层次优化技术的XACML策略评估引擎

给出一种采用多层次优化技术的XACML(extensible access control markup language)策略评估引擎实现方案MLOBEE(multi-level optimization based evaluation engine).策略判定评估前,对原始策略库实施规则精化,缩减策略规模并调整规则顺序;判定评估过程中,在引擎内部采用多种缓存机制,分别建立判定结果缓存、属性缓存和策略缓存,有效降低判定引擎和其他功能部件的通信损耗.通过两阶段索引实现的策略缓存,可显著降低匹配运算量并提高策略匹配准确率.仿真实验验证了MLOBEE所采用的多层次优化技术的有效性,其整体评估性能明显优于大多数同类系统.

正确性保证的私有过程建模方法

私有过程是构建协同业务过程基础,其正确与否对业务协同实施产生直接影响.为此,提出了一种逐步求精构建私有过程的方法.首先,定义私有过程,并将其控制流抽象为四种基本块,即顺序块、并发块、选择块及迭代块;然后,针对四种基本块提出各自的精化规则,并以此为基础提出了私有过程构建方法;最后,从理论上证明了通过该方法建立的私有过程具有工作流网特性且是正确的.通过对协同制造中供应链建模并与现有的、典型的方法对比分析,结果表明:相对已有的工作,本文方法能够更加有效地对私有过程进行建模.