CAJ | 학술논문

文章针对软件验证过程中的结构抽象表示问题，考虑到结构程序的顺序结构、调用返回关系，给出了嵌套树以及嵌套状态机的定义。在该数据结构及μ演算的基础上，定义了嵌套树的μ演算（N T‐μ）。N T‐μ的公式语法是基于概要的，在嵌套状态机上提出基于概要类的模型检测。嵌套状态机的结点是有限的，且嵌套状态机有限的概要类对应于嵌套树中的无限的概要，因此该方法能提高检测的效率。
문장침대연건험증과정중적결구추상표시문제，고필도결구정서적순서결구、조용반회관계，급출료감투수이급감투상태궤적정의。재해수거결구급μ연산적기출상，정의료감투수적μ연산（N T‐μ）。N T‐μ적공식어법시기우개요적，재감투상태궤상제출기우개요류적모형검측。감투상태궤적결점시유한적，차감투상태궤유한적개요류대응우감투수중적무한적개요，인차해방법능제고검측적효솔。
To solve the problems of structure abstract representation in the software verification process ,taking into account the program sequence structure and the relationship between call and re‐turn ,the definition of nested trees and nested state machine is given .Based on the data structure andμ‐calculus ,the μ‐calculus of nested trees(NT‐μ) is defined .The formula syntax of NT‐μis based on the summary ,and the model checking of summary class is presented .For the reason that the nodes in the nested state machine are finite ,and the finite summary class in the nested state machine corre‐sponds to the infinite summary in the nested tree ,the method can improve the detection efficiency .