程序切片技术在并发程序模型检查中应用.pdfVIP

第 l8卷 第 lI期 计 算 机 技 术 与 发 展 Voll8 ()．¨ 2008年 IJ月 C0MPUTER TECHNOIX；Y AND DEVEI PMENT NOV． 2008 程序切片技术在并发程序模型检查中的应用 高鹏飞，沈云付 (上海大学 计算机工程与科学学院，上海 200072) 摘 要：模型检查技术在硬件和协议设计方面已经取得很大成功，但在软件验证方面仍存在很多困难。其主要问题是如 何从源代码中自动抽取验证所要模型并精简其状态空间。文中通过对程序切片技术的研究，来解决并发程序验证的建模 问题 ，包括把验证公式映射到切片准则 ．并把得到的程序切片转化为验证所需的模型。经程序切片处理后，软件模型检查 效率得到提高。 关键词：并发程序；模型检查；程序切片 ；状态空间；切片准则 中图分类号 ：TP301．2 文献标识码：A 文章编号：1673—629X{2008)11—0163—05 ApplicationofProgram SlicingTechnologytoConcurrent ProgrammingM odelChecking GAO Peng—fei，SHEN Yun—fu (Sch．ofComputerEngineeringandScience，ShnaghaiUniversity，Shmlghai200072，China) Abstract：Despitethesuccessofmodelcheckingforhardwareandprotocoldesign，thereremanydifficultiesinsoftwaremodelchecking． Themainproblem isautomaticextractionofn~ elsfrom codesnadhowtOrdeucethestatespaceofthemodelextractedfrom codes．An applicationofprogram slicingtOhnadletheissuesmentionedaboveispresented，whichincludehow tomapthespecificationusedinmodel checkingtotheslicingruleandhow totransfertheslicesoftheprogram tothemodelforchecking．Theresulteisthatitisanefficient waytoimprove．softwaremodelchceking Keywords：concurrentpmgrnam~ing；~dtwaremodelchceking；program slicing；statespace；slicing criterion 0 引 言 1 软件模型检查和程序切片技术现状 随着信息化的普及，软件已经广泛应用于各个领 1．1 软件模型检查现状 域，其中包括对安全性要求较高的领域。软件技术的 目前对程序建模的方法主要有两种，一种是程序 发展使得软件系统的结构越来越复杂，复杂度越来越 标号法l，另一种是程序控制流图法 2。 高，而软件的可靠性却未能得到提高。传统的测试方 程序标号算法是通过假设每一条语句都有唯一的 式显然不能有效地解决这个问题，从逻辑角度讲，可 以 人点和出点，这样的唯一标注可 以简化迁移程序 。每 通过测试找出错误，但无法宣称该软件在任何情况下 个语句的出点与紧随其后语句的入点是一致的。模型 都无错，因此形式化验证方法开始受到重视 。目前常 中状态由变量值和语句位置组成，状态迁移由