没有合适的资源?快使用搜索试试~ 我知道了~
动作系统改进的自动验证方法
理论计算机科学电子笔记187(2007)75-90www.elsevier.com/locate/entcs用于检查动作系统改进的格雷姆·史密斯1 Kirsten Winter2澳大利亚昆士兰大学信息技术与电气工程学院摘要动作系统提供了一个正式的方法来模拟并行和反应系统。他们有一个完善的理论,由基于模拟的证明规则支持。本文介绍了一种利用标准CTL模型检查来验证动作系统改进的自动方法。为此,我们将每个模拟条件编码为模拟机,一种Kripke结构,通过检查相关CTL属性是否成立,可以履行证明义务。该过程将每个仿真条件转换为模型检查问题。然后,可以单独地对每个仿真条件进行模型检查,或者如果需要,可以通过组合仿真机和CTL属性与其他仿真条件一起进行模型检查。关键词:精化,模型检测,动作系统,CTL。1引言动作系统[2]是并行和反应系统的规范化和逐步定义的成熟形式主义。它们能够对具有终止、非终止和中止行为的系统进行建模。动作系统精化[3,1]是根据顺序精化演算[5]定义的。这是一个非常普遍的细化概念,允许在每个细化步骤中对系统的设计进行重大更改,即,动作的数量和特定动作的角色可以完全改变。这是通过划分抽象的和具体的具体化,分为那些外部可观察的和那些内部口吃的行为。Back和von Wright [4]提出了基于仿真的动作系统改进1 电子邮件地址:smith@itee.uq.edu.au2电子邮件:kirsten@itee.uq.edu.au1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2006.08.04576G. 史密斯,K.Winter/Electronic Notes in Theoretical Computer Science 187(2007)75对支持细化的工具的需求得到了充分的认可。如果没有这种支持,除了最关键的系统之外,对所有系统进行改进都是不切实际的。传统上,这样的工具支持已经基于交互式定理证明器。这包括对动作系统的显式支持[14],以及精化演算[7]。最近,自动验证技术的进步,包括决策过程和模型检查,已经看到了全自动方法来验证改进的步骤[11,6,12]。特别是,Smith和Derrick [12]展示了如何在标准模型检查器中编码Z细化的模拟证明义务。在本文中,我们对更一般的动作系统改进采用了类似的方法:而不是将抽象和具体系统直接编码到模型检查器中,我们将每个模拟条件编码为Kripke结构或总状态转换系统,称为模拟机以及在分支时间时序逻辑CTL中形式化的属性[10]。这是以这样一种方式完成的,即证明义务恰好在CTL属性对模拟机成立时成立。后者可以使用CTL模型检查器自动验证。这种方法避免了在大多数情况下构建两个系统的整个状态空间的需要,并简化了需要检查的属性。本文的组织如下:在第2节中,我们提供了一个动作系统和动作系统精化的概述,以及对时序逻辑CTL的简要介绍。在第3节中,我们将讨论将动作系统模拟条件表示为模型检查问题的方法,并提出我们的方法。在第4节中,我们通过案例研究及其在SAL模型检查工具的输入符号中的编码来说明我们的方法[9]。最后,我们将在第5节讨论局限性和未来的工作。2预赛2.1行动系统动作系统[2]是一种对并行和反应系统进行建模的形式主义。动作系统模型描述了一个由初始化和一组动作组成的机器,每个动作都是一个受保护的命令(包括一个保护,当满足时启用动作,以及一个语句)。这些操作将重复执行,直到没有任何操作被启用,机器终止。动作系统A具有以下形式:A =|[varx:X·x:= x0;做A1[]. [] Anod]|:z:Z一个动作系统的状态有两个组成部分,局部状态和全局状态。在上面的A中,局部状态由X类型的变量x给出,该变量被初始化为x0。全局状态由Z类型的变量z给出。动作A1,. . ,An以交错方式执行:其中一个启用的操作是G. 史密斯,K.Winter/Electronic Notes in Theoretical Computer Science 187(2007)7577QQ在每一步都不确定地选择,直到没有一个动作被启用。如果系统的最终操作终止,则系统终止。如果在其最终操作中,语句的前提条件失败,并且操作无法终止,则系统中止。机器A可以被看作一个元组(A0,A),带有初始化命令A0和动作A,其中A是上面的do od循环中单个语句的组合。初始化条件用PA0表示。同品种器械nA表示总是终止语句A的下一状态关系。 动作A的使能保护表示为gA:只要gA满足,动作A就可以执行。因此,谓词<$gA模拟了动作A的终止。动作A的终止保护被表示为tA。它模拟动作A正确终止。否定<$tA模拟动作A正在中止。DOA表示A的迭代的终止保护,即, DOA=doAodtrue。 An是迭代动作A n次的简写,An是对A的所有n次迭代的恶魔选择。A中的一些动作被挑出来作为口吃动作Aq。 口吃动作总是终止并保持全局状态不变,即,nAq(a,u)(aJ,uJ)<$(uJ=u).不结巴的行为被称为改变行为A。2.1.1动作系统细化为了证明抽象系统A=(A0,A)与一个更具体的系统C=(C0,C),Back和vonWright介绍了基于模拟的证明规则[4]。设R表示C的状态与A的状态之间的抽象关系。如果A和C中的动作可以分解为变化动作和断续动作,使得以下模拟条件成立,则抽象系统A可以由具体系统C(i) 在C中,任何初始化后跟随着口吃动作的动作都模拟了A中的初始化后跟随着口吃动作的动作。pC0(c,u)nCm(c,u)(cJ,uJ)(一)QA,A,J. R(aJ,cJ,uJ)<$pA0(a,u)<$nAn(a,u)(aJ,uJ)(ii) C中的任何更改操作后接断续操作都模拟A中的某个更改操作后接断续操作。R(a,c,u)<$(nC;nCm)(c,u)(cJ,uJ)(二)QtA(a,u)R(aJ,cJ,uJ)<$(nA;nAn)(a,u)(aJ,uJ))(iii) C中的任何中止状态都与A中的中止状态相关。(三)R(a,c,u)<$tC(c,u)<$tA(a,u)(iv) C中的任何终止状态都与A中的终止或中止状态相关。[3]动作系统的痕迹语义学捕捉的是计算性的,而不仅仅是输入-输出,系统行为。78G. 史密斯,K.Winter/Electronic Notes in Theoretical Computer Science 187(2007)75(四)R(a,c,u)<$<$gC(c,u) <$tA(a,u)(v) C中任何可能出现无限口吃的状态都与一个正在流产或可能发生无限口吃的疾病(五)R(a,c,u)DOCq(c,u)tA(a,u)DOAq(a,u)如果我们能证明抽象系统A和具体系统C的这些模拟条件,那么迹加细A±C是有效的。这种方法被称为正演模拟。也存在反向模拟的模拟条件。然而,到目前为止,我们的结果只考虑了正向模拟条件。反向模拟条件的模型检验将是我们未来工作的一个问题。2.2时序逻辑CTLCTL [10]是一个分支时间时序逻辑,它是相对于Kripke结构定义的。一个Kripke结构是一个具有全转移关系的状态转移系统。设M是一个Kripke结构,V是一组原子命题. 一标记函数L将M中的每个状态映射到原子命题的集合,满足于国家。有效的CTL公式与M中的状态s相关,即,它是一个由状态和路径公式构建的状态公式:CTL的定义2.1状态公式:(一)如果n∈ V,则n是一个状态公式。(二)如果和是状态公式,则和是状态公式。(三)如果E是一个路径公式,那么E是一个状态公式。路径公式:(一) 如果和是状态公式,则X和U是路径公式。E是路径的存在性量化器,X指的是下一个状态,U是路径的直到运算符:U表示为真,直到为真(并且必须最终为真)。 一些额外的运算符用作缩写:布尔运算符:⇔)和⇔最终,F惠(真正的U惠),总是:G惠<$F <$,和普遍的量化器在所有paths(for all paths):一个优惠<$E <$。从上面的语法定义中,可以导出三个基本的时态逻辑运算符来建模状态公式,EX,EU和EG。CTL状态公式的语义在状态公式的结构上归纳定义如下:G. 史密斯,K.Winter/Electronic Notes in Theoretical Computer Science 187(2007)7579⎨定义2.2 CTLS|=惠∈L(s),如果∈ VS|=<$优惠s|=S| = 100万美元|= 101或s| = 100.有一条路径π,从状态s开始,S| = EX优惠s1是π中的下一个|= ϕ holds有一条路径π,从状态s开始,使得S| = E(1U2)惠存在k≥ 0,且sk|2,且对于所有0 ≤j为了避免两个模型之间的名称冲突,我们使用前导88G. 史密斯,K.Winter/Electronic Notes in Theoretical Computer Science 187(2007)75a(抽象模型中的变量)和c(具体模型中的变量因此,变量Cr。0被编码为ccr0。编码中出现的唯一复杂性是类型必须是有限的。虽然SAL确实支持有限类型,但一般来说,模型检查器只适用于有限类型5。 我们限制了PC的类型。我是0…3,y的。i和w为0…10个。为了对第3.2节中给出的完整模拟机进行编码,我们定义变量p:1 6。它允许我们将机器的行为限制在我们的意图之内。例如,BS。0是C中的口吃动作,即,属于Cstutt。我们必须相应地将其出现限制在p∈{1, 4, 5}的相位。C中的断续动作不会导致模拟机改变其相位,即,p保持不变:BS 0:(p=1或p=4或p=5)和ccr0AND cpc0=0-->在我们的模拟机中,动作CChange由动作CSJ给出。i和NS。iinC以上对于进程0,这些被编码如下:CCS 0:p=3且cpc0=2且(非(cb1)或ct=1)-->和CNS 0:p=3且NOT(ccr 0)--> ccr 0 ' IN { b:布尔|return true};请注意,在行动CNS0中,变量ccr 0的下一个状态值是非决定性地选择的。这两个动作都将仿真机的相位更改为p=4。仿真机还包含跳过转换,这些跳过转换不改变动作系统中的任何变量,但可能改变仿真机中的相位。例如,从相位p= 3到p= 5的跳跃被编码为:p=3-->然后,使用SAL选择运算符[]将抽象和具体系统的编码操作组合在一起。精化关系R以及CTL属性中使用的所有谓词(即,Aaborting、Aterminating、CInit、Caborting和Cterminating)被编码为对系统状态变量的定义。在仿真机的任何阶段,它们都可以被评估为真或假,例如,在一个实施例中,CInit= cb0= AND cb1= AND cpc0=0 AND cpc1=0 AND ccr0 = AND ccr1=;为了对终止条件进行编码,我们否定了相关守卫的析取。为了对中止条件进行编码,我们将相关保护的合取与相关联的语句不可能的条件分开,例如,5 SAL有一个有界模型检查器,它可以处理无限类型。G. 史密斯,K.Winter/Electronic Notes in Theoretical Computer Science 187(2007)7589我们的行动BS0(ccr 0ANDcpc 0 =0) ANDFORALL(a:BOOLEAN,b:ProgramCounter):NOT(a ANDb=1)其中ProgramCounter是类型03. 案例研究的完整编码可以在[13]中找到。可以检查与用于本案例研究的完整正演模拟精化检查的模拟机相关的属性是否有效。在一台配备3GHz Intel Pentium 4处理器和512MB RAM的PC上,检查过程在3.55秒内终止。5结论我们提出了一种自动验证动作系统细化的方法。虽然之前已经有研究Z类精化的自动验证的工作[11,6,12],但据我们所知,这是更一般的动作系统精化的第一种方法我们的方法可以与任何CTL模型检查器一起使用,尽管对动作警卫和高级构造(如量化器)的显式支持使得SAL模型检查器特别适合。我们有兴趣以两种方式扩展这项工作的适用性首先,我们只考虑了前向模拟。这是迄今为止最常见的细化形式,但为了完整起见,我们希望将我们的工作扩展到也包括向后模拟。其次,我们被限制在类型有限且不太大的系统中;否则模型检查变得不可行。然而,这些限制可以通过利用模型检查领域的最新进展来解除,例如,自动谓词抽象[8]或有界模型检查[9]。我们对前者特别感兴趣,并利用我们希望证明的系统结构(就阶段而言)和性质是固定的这一事实来简化抽象过程。确认我们感谢澳大利亚研究委员会(ARC)发现补助金DP0345355和DP0558408的支持。引用[1] R.J. R回来了改进并行和反应式程序。技术报告Caltech-CS-TR-92-23,计算机科学系,加州理工学院,1992年。[2] R.J. R巴克和R.库尔基-苏尼奥过程网络的分散化与集中控制。Distributed Computing,3(2):73[3] R.J. R 贝克街和K街。塞尔并行算法的叠加精化在K。Parker和G.Rose,editors,FormalDescription Techniques(FORTE IV),pages 475北荷兰,1992年90G. 史密斯,K.Winter/Electronic Notes in Theoretical Computer Science 187(2007)75[4] R.J. R巴克和J·冯·赖特。动作系统的跟踪细化。芽孢杆菌中Jonsson和J. Parrow,编辑,并发理论(CONCURSpringer-Verlag,1994.[5] R.J. R巴克和J·冯·赖特。精化演算:系统介绍。计算机科学研究生教材。Springer-Verlag,1998.[6] C. 博尔顿使用合金分析仪验证Z中的数据细化在j.Derrick和E.Boiten,编辑,REFINE 2005,第137卷,ENTCS第2期,第23Elsevier,2005年。[7] M.作者声明:J.朗巴卡河Ruksenas,and J. von Wright. 精化计算器:对程序精化的证明支持。在洛Groves和S. Reeves,editors,Formal Methods Paci ficSpringer-Verlag,1997.[8] E. Clarke,O.Grumberg,S.Jha,Y.Lu和H.维斯反例引导的抽象在东亚。Emerson和A. P. Sistla,编辑,计算机辅助验证国际会议(CAVSpringer-Verlag,2000.[9] L. de Escherichia,S.奥雷Rushby,N.尚卡尔,M。Sorea和A.蒂瓦里 SAL 2. In R.布雷尔和D. Peled,编辑,计算机辅助验证国际会议(CAV 2004),LNCS第3114卷,第496-500页。Springer-Verlag,2004.[10] E.A.爱默生时态和模态逻辑。在J. van Leeuwen,编辑,Handbook of Theoretical Computer Science,卷B,第996-1072页中。Elsevier Science Publishers,1990.[11] M. Leuschel和M.管家B的自动微调检查。在K。Lau和R.巴拿赫,编辑,形式工程方法国际会议(ICFEM2005),LNCS第3785卷,第345-359页。Springer-Verlag,2005.[12] G. Smith和J.德里克模型检查向下模拟。在j.Derrick和E.Boiten,编辑,REFINE 2005,第137卷,ENTCS第2期,第205-224页。 Elsevier,2005年。[13] G. Smith和K.冬天用于检查动作系统改进的模拟机器。技术报告SSE-2006-03,昆士兰大学信息技术与电气工程学院,2006年。[14] M.我们会去 的 。 先 生 。在 B-TOL 中 与 他 一 起 重 新 定 义 操 作 系 统 。 在 FormalMethodsEurope(FME'96),LNCS的第1051卷,第84-103页中Springer-Verlag,1996.
下载后可阅读完整内容,剩余1页未读,立即下载
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![application/x-rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![pptx](https://img-home.csdnimg.cn/images/20210720083543.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- VMP技术解析:Handle块优化与壳模板初始化
- C++ Primer 第四版更新:现代编程风格与标准库
- 计算机系统基础实验:缓冲区溢出攻击(Lab3)
- 中国结算网上业务平台:证券登记操作详解与常见问题
- FPGA驱动的五子棋博弈系统:加速与创新娱乐体验
- 多旋翼飞行器定点位置控制器设计实验
- 基于流量预测与潮汐效应的动态载频优化策略
- SQL练习:查询分析与高级操作
- 海底数据中心散热优化:从MATLAB到动态模拟
- 移动应用作业:MyDiaryBook - Google Material Design 日记APP
- Linux提权技术详解:从内核漏洞到Sudo配置错误
- 93分钟快速入门 LaTeX:从入门到实践
- 5G测试新挑战与罗德与施瓦茨解决方案
- EAS系统性能优化与故障诊断指南
- Java并发编程:JUC核心概念解析与应用
- 数据结构实验报告:基于不同存储结构的线性表和树实现
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)