CAJ | 학술논문

模型构建是模型检验的基础,在微控制器代码模型构建过程中面临状态爆炸的问题.由于生成模型的状态数量与代码规模密切相关,通过简化代码可以有效缩减生成的状态数量.该文提出了敏感变量和敏感位置的概念,并以此为基础提出了结合子程序信息的敏感位置识别算法;该算法从待验证的性质出发,提取敏感变量,识别代码中与敏感变量相关的敏感位置;模型构建过程中只对敏感位置对应代码进行建模,从而实现对模型状态的缩减.实验结果表明所提的方法能够有效缓解微控制器代码模型生成过程中的状态爆炸问题.
모형구건시모형검험적기출,재미공제기대마모형구건과정중면림상태폭작적문제.유우생성모형적상태수량여대마규모밀절상관,통과간화대마가이유효축감생성적상태수량.해문제출료민감변량화민감위치적개념,병이차위기출제출료결합자정서신식적민감위치식별산법;해산법종대험증적성질출발,제취민감변량,식별대마중여민감변량상관적민감위치;모형구건과정중지대민감위치대응대마진행건모,종이실현대모형상태적축감.실험결과표명소제적방법능구유효완해미공제기대마모형생성과정중적상태폭작문제.
Model construction is the basis of model checking. State explosion can not be avoided during building model for microcontroller code. Because the state number of generated model is related to code size, the number of state can be reduced through simplifying microcontroller code. An algorithm of sensitive position identification with subroutine summary information is proposed, based on concepts of sensitive variable and sensitive position. Sensitive variables are extracted from verified properties and used to identify sensitive positions. Then model is constructed from code corresponding to sensitive positions. Experimental results show that the problem of state explosion can be effectively alleviated through the proposed method.