基于嵌套树的对等博弈应用研究

摘要：

进行了软件系统性质验证研究.首先提出了用嵌套树表示软件程序的方法,以解决软件系统的抽象表示问题,该方法能在表示程序顺序结构的同时,更好地表示调用返回关系.然后定义了嵌套树上的μ-演算,以便将要验证的需求性质用公式表示,并把公式转化成非确定对等嵌套树自动机.最后将自动机与嵌套树结合,转化形成博弈图,并用对等博弈条件来判断博弈的输赢,这等同于检验验证公式是否在嵌套树上成立.相比直接验证,这种判定方法表达更为直观,且更有利于整个过程的自动化.研究表明,将嵌套树中的调用关系展开可形成概要标签树,嵌套树的对等博弈理论也可以应用到概要标签树中.

关键词：对等博弈、嵌套树、交替树自动机、μ-演算、概要

所属期刊栏目：25

分类号：TP3;G25

资助基金：国家自然科学基金61075002;国家科技支撑计划重大项目2011BAG01B03;863计划2012AA112801

在线出版日期：2016-03-17（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：895-904