欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
进行了软件系统性质验证研究.首先提出了用嵌套树表示软件程序的方法,以解决软件系统的抽象表示问题,该方法能在表示程序顺序结构的同时,更好地表示调用返回关系.然后定义了嵌套树上的μ-演算,以便将要验证的需求性质用公式表示,并把公式转化成非确定对等嵌套树自动机.最后将自动机与嵌套树结合,转化形成博弈图,并用对等博弈条件来判断博弈的输赢,这等同于检验验证公式是否在嵌套树上成立.相比直接验证,这种判定方法表达更为直观,且更有利于整个过程的自动化.研究表明,将嵌套树中的调用关系展开可形成概要标签树,嵌套树的对等博弈理论也可以应用到概要标签树中.
英文摘要：
The nature verification of software systems was studied. Firstly, a method for program representation based on a nested tree was proposed to tackle the abstract representation problem of a software system. The method can indi- cate the program sequence structure, and can better represent the relationship between call and return. Then, the/.~ -calculus of the nested tree was defined to formulize the requirement nature to be verified and to transfer the formula into a nondeterministic parity nested tree automation. Finally, the automation was combined with the nested tree to form a game graph, and the parity game conditions were used to determine the games winners and losers, which is equivalent to testing whether the validation formula is satisfied in the nested tree. Compared with the direct verifica- tion, the above-stated method is more audio-visual and more beneficial to process automation. The study shows that the call-return relation can be expanded to form a summary tag tree, and the parity game theory can be well applied to the summary tag tree.
同期刊论文项目
同项目期刊论文
期刊信息
位置：