学习模型检测与测试模型验证器的研究-程序分析系统ROPAS的实践应用

34理论计算机科学电子笔记43（2001）网址：http://www.elsevier.nl/locate/entcs/volume43.html16页学习模型检测的谜题，编程模型检测的谜题，测试模型验证器N. V.Shilov1、2、4和K.Yi1，3程序分析系统ROPAS的研究韩国科学技术高等研究院Kusong-dong Yusong-gu 373-1Taejon 305-701，大韩摘要本文讨论了一些问题，有限游戏的早期正式的方法教学和验证的自动工具，实现正式的方法的实用程序。特别是，一些经验（1）本科教学模型检查通过有限的游戏，（2）解决基于游戏的约束通过模型检查，（3）测试模型检查器对游戏测试套装。基本思想是通过一个基于模型检测的解决方案来说明的，该解决方案解决了一个复杂的难题，即如何在给定的硬币中识别出一个唯一的假币，并在有限的时间内平衡1介绍形式化方法在计算机硬件和软件开发中的作用越来越大，因为系统变得越来越复杂，需要更多的工作来规范、设计、实现和验证。与此同时，形式化方法变得更加复杂，因为它们必须捕获真实系统的真实属性以进行合理的推理。形式化方法的综述不在本文的讨论范围之内。获得关于形式化方法研究的范围和范围及其工业应用的意见的最好方法是1这项工作得到了韩国科学部创造性研究倡议的支持和技术2 电邮地址： shilov@ropas.kaist.ac.kr主页：http://ropas.kaist.ac.kr/~shilov3电邮地址：kwang@ropas.kaist.ac.kr主页：http://ropas.kaist.ac.kr/~kwang4在离开AP西伯利亚分部信息系统研究所俄罗斯科学院，新西伯利亚，俄罗斯2001年由ElsevierScienceB出版。 V. 操作必须符合C CB Y-NC-N D要求。希洛夫和伊35特 别 访 问网 站牛 津 大 学 的 http://archive.comlab.ox.ac.uk/formal-methods.html或NASA的http://shemesh.larc.nasa.gov/fm/。尽管如此，我们还是要指出，在形式方法中使用的规范语言从命题到高阶不等，而证明技术要么是语义（模型检查），要么是句法（演绎）推理。特别是，程序逻辑是用于硬件和软件验证和规范的模态逻辑在命题程序逻辑的多样性中，一个特殊的位置属于D的命题微演算（µ”[17]《孝经》云：“孝，孝也。简而言之，µC可以定义为基本模态逻辑K的多模态变体，带有定点。对于μ C的模型检验问题是一个非常重要的研究课题[9，1，10，12，2，24，25，6，7，23，11]。模型检验的μ-演算和特殊的双模拟游戏之间的密切关系已经在文献[24，25，23]中进行了研究特别是，[24]定义了μC的无限模型检查游戏，[25]定义了有限定点游戏，并通过μC公式在获胜策略方面描述了过程（状态）的不可重复性，[23]利用模型检查游戏进行实际有效的局部模型检查。我们想讨论与博弈在微积分中的作用有关的另外三个问题，即：• 用于模型检查早期教学的有限游戏（第2，3节），• 模型检查编程获胜策略（第4，5节），• 通过有限游戏测试套装验证模型检查器（第6节）。2通过游戏学习微积分尽管正规方法对于开发可靠的硬件和软件的重要性，但非专业人员对该研究领域并不熟悉特别是，许多与计算机硬件和软件（即纯/应用数学和电气/电子工程）的进一步发展密切相关的系的本科生认为形式方法一般不在他们的兴趣范围内，因为它们（形式方法）• 要么是太穷了，学不了纯数学，• 要么是太纯了，不适合他们可怜的数学我们特别关注这种令人失望的没有很好动机的态度，并假设缺乏关于这个主题的流行讲座，教程和论文是这种无知的主要原因但是，研究人员采用正式方法推广其研究领域的态度似乎并不比学生采用正式方法的态度好多少，而研究的大众化呈现是更好的计算机科学教育的好机会，并将支持科学研究向工业实践的转移实际上，与学者们对普及其研究的态度相比，希洛夫和伊36·计算机科学家们似乎并不令人印象深刻。有几个流行的世界知名的数学杂志的学生以及研究人员（例如，美国数学月刊（American MathematicalMonthly）此外，数学家越来越关注学生中应用数学的普及。特别是，工业与应用数学学会（SIAM）最近在SIAM评论（SIREV）中推出了一个关于教育的特别部分正如SIREV作者中所述，在大多数情况下，文章应该为学生而不是教师写。 文章应该提供描述，插图和景点，re-garding建立或最近的知识，而不是新的研究成果。相比之下，很难指出一个定期为学生发表流行和临时论文的计算机科学期刊。上述论点可能会导致一个结论，即对形式方法理论的大众化持否定态度这个结论当然是无效的。真的，让我们只是提醒国际暑期学校在Markto-berdorf和欧洲暑期学校在逻辑，语言和信息。但让我们也注意到，这些学校的听觉是比较小的（每年几百），由研究生或研究生，初级科学家或教授。通过流行的（但合理的）形式化方法的数学基础的介绍，早期和更好的教学形式化方法游戏和基于游戏的谜题的教育作用在计算机科学知识逻辑的文献中得到了广泛的认可例如，在[13]中，基于知识的muddy childrenpuzzle分析，同步攻击和拜占庭协议激发并说明了基本的理论思想和概念。教育工作者/研究人员应该从中吸取的主要教训[13]是：为了吸引人，形式方法的数学基础应该通过具有挑战性的基于游戏的例子来说明我们想在下面描述一下，在准备ACM大学生编程竞赛期间，如何以一种流行的（但数学上合理的）形式向新西伯利亚国立大学数学、物理和技术系的本科生介绍一种称为形式方法的强大流的程序逻辑支流。我们希望这个例子不仅从教学的角度来看，对模型检测社区来说也是有趣的，因为它有助于理解和发展一些进一步的结果。本文的第一作者是区域中学数学竞赛计划委员会的成员。几年前，委员会向参加比赛的学生提出了以下难题一套硬币由14枚有效硬币和1枚假币组成。所有有效的硬币都有相同的重量，而假币有另一个重量。其中一个有效硬币被标记，而所有其他硬币（包括假硬币）都没有标记。是否最多3次就能识别假币？希洛夫和伊37··•≥ ≥≥两位作者都是ACM区域编程竞赛本科生团队的培训师。 因此，如何解决编程难题的问题自然出现了。最后设计了一个相应的程序设计问题，并在培训班上推荐给本科生。问题的简要形式如下：编写一个具有3个输入的程序ALPHA- 所讨论的N个硬币-M 个标记的有效硬币，- 平衡极限K其输出不可能的或另一交互式程序BETA（用相同的语言），该交互式程序BETA实现K次（最多）平衡策略，用于在M个标记的有效硬币的帮助下识别N个硬币中的单个假币。每次测试都应该从用户为一枚假币选择一个数字开始，无论它是轻还是重。则一个会话由一系列轮组成，一般轮数不能超过K。在每一轮的程序输出两个不相交的子集的硬币数量被放置在锅的平衡。轮到用户根据初始选择进行回复会话以BETA的最终输出--假币的数量结束由于问题是写一个程序，产生另一个程序，那么我们想把第一个程序称为元程序，把问题分别称为元程序问题为了解决元程序问题，让我们给出一个游戏解释：令 M 和 N 是 非 负 整 数 参 数 ， 并 且 令 （ N + M ） 个硬 币 由 数 字 [1.（N+M）]。数字硬币[1] [1]是一个伪命题，而[2]是一个伪命题，[3]是一个伪命题。（M+N）]。两个玩家user和prog的GAME（N，M）由一系列回合组成。在每一轮上，prog的移动是[1.]的一对不相交的子集（具有相等的基数）。（M+N）]。用户的可能移动是<、=或>，但移动必须与前几轮中引入的所有约束一致 Prog赢得游戏（N，M）尽快在[1.. （M+N）]满足博弈过程中引入的所有约束。在这些设置中，元程序问题可以重新表述如下：写一个程序，对所有的N1，K0和M0，在博弈（N，M）中产生（不可能）一个最多K轮的获胜策略然后另一个问题出现了：什么是一个适当的形式主义的元语法问题，在这个新的设置？一个提示是，形式主义应该有明确的要点。实际上，下面的非正式陈述是非常自然的：如果一个玩家prog处于他/她有获胜策略的位置，那么他/她在游戏没有输的之前和之后都有一个移动，但是在这之后另一个玩家用户的每一个移动都会导致游戏输或prog有获胜策略的位置换句话说：一组位置，其中prog有一个获胜希洛夫和伊38∨--|¬∧⟨ ⟩策略是对位置集合进行特殊操作的定点函数式范式是一个众所周知的具有显式定点的范式。但是，根据ACM大学程序设计竞赛的规定，程序应该用命令式语言（如PASCAL）编写。所以在这种情况下，另一种范式会比功能范式更好它应该是一个同时捕捉命令式风格和固定点的范式。这是一个程序逻辑的范例，特别是命题微演算的形式但是这种形式主义并不十分简单，因为在最全面的形式中，它依赖于transfinite归纳法：要使微积分对本科生来说容易并不容易！另一个提示是引入µ-Calculus的增量方法，以及仅在有限模型中对µ-Calculus进行模型检查参见[21]，了解元程序问题的完整解决方案和背景理论的细节，而在第3，4，5节中给出了简要的总结3通过游戏实现设true，false为布尔常量，Prp和Act分别为命题变量和动作变量的不相交有限个alpha- bets经典命题逻辑的语法由公式组成，并根据标准规则由命题变量和布尔连接词（否定），（合取）和（析取）构造初等命题动态逻辑（EPDL）[15]有额外的特征来构造与动作变量相关的公式-模态：如果a是动作变量，φ是公式，则（[a]φ）和（a φ）是公式5。EPDL的语义在模型中定义，称为过渡系统或Kripke结构。模型M是一对（DM，IM），其中定义域DM是一个非空集，而解释IM是一对特殊映射（PM，RM）.定义域DM的元素称为状态。解释将命题变量映射为状态集，将动作变量映射为二进制国家关系PM：Prp→ P（DM） 、R M：Act→ P（D M× D M）其中P是功率设置操作。我们写IM（p）和IM（a），而不是PM（p）和RM（a），只要它隐含p和a是命题变量和动作变量。模型可以被认为是带有标记的图，节点和边分别由命题变量和动作变量的集合对于每个模型M=（DM，IM），状态和公式之间的有效性关系=M可以根据公式的结构归纳地定义对于布尔常量，命题变量和命题连接词语义是以标准的方式定义的，而我们有1. S|= M（α<$φ）i <$（s，sJ）∈ I M（a）且sJ|= Mφ对于某个状态SJ，5分别读作希洛夫和伊39∈≥2. S|= M（[a] φ）i <$（s，sJ）∈ I M（a）蕴涵sJ|= Mφ对于每个状态sJ。因此，一个有经验的数学家可以说EPDL只是基本命题模态逻辑K[3]的一个多模态变体有限博弈可以说明所有与EPDL相关的概念。一个有两个局A和B的有限对策是一个元组（P，MA，MB，F），其中• P是一个非空的有限位置集合，• MA，MBP×P是A和B的（可能）移动，• FP是一组最终位置。游戏的一个会话是一个位置序列s0，... sn，. 其中所有偶数对都是一个平面的多个（例如， all（s2i，s2i+1）∈MA），而所有奇对都是另一个平面的运动（例如，all（s2i+1，s2i+2）MB）。在一个回合中，两个玩家的一对结果移动包括三个结果位置（例如，（s2i，s2i+1，s2（i+1））称为round。当一名球员移动一次后，该球员失去一个会话，该会话第一次进入最终位置一个玩家赢得了一个会话，而另一个玩家失去了会话。参与人的策略是参与人可能的行动的子集玩家的获胜策略是玩家的策略，它总是导致玩家获胜：玩家赢得他/她开始的每个会话，并且他/她执行此策略而不是所有可能的上述类型的每一个有限对策（P，MA，MB，F）都可以自然地表示为有限Kripke结构G（P，MA，MB，F）• 状态是位置P，• 动作变量moveA和moveB被解释为MA和MB，• 命题变量fail被解释为F。命题3.1设（P，MA，MB，F）是两个局中人的有限对策，设WIN0是一个公式false，对于每个i≥1，设WINi+1是一个公式<$failmove A（<$fail [move B]（fail WIN i））.• 对于任意i0，公式WINi在G（P，MA，MB，F）其中参与人A最多有i轮的获胜策略• 对于每个i>0，参与人A的每个i轮最多获胜策略的第一步包括移动到位置，在该，<$fail [移动B]（failWIN i-1）有效。设无限析取i≥0WIN i，语义i≥1{s：s| = MWIN i}在模型M中是EPDL一个特殊的扩展• 在G（P，MA，MB，F）的那些态中，无穷析取i≥0WINi参与人A有一个获胜策略• 无限析取i≥0WINi是EPDL的非法公式，等同于EPDL的任何公式命题3.1自然引出以下建议让我们定义作为EPDL扩展的命题μ-Calculus有两个新特性：希洛夫和伊40ppp|pp赢得WIN i-1（false））有效。pp赢得赢得如果p是命题变量，φ是公式，则（μp.φ）和（νp.φ）是公式6。 我们还想强加以下上下文敏感的限制：命题变量的有界实例不能是负的。非正式地说，μp.φ是无限析取的“缩写”。falseφ p（false）φ p（φ p（false））φ p（φ p（φ p（false）. 为而νp.φ是另一个true<$φ p（true）<$φ p（φ p（true））<$φ p（φ p（φ p（true）<$. =i≥0i≥0i（false）φi（true），其中φ p（φ）是φ中代入φ而不是p的结果，φ0（φ）是φ，并且φi+1（φ）isφp（φi（φ）），其中i≥0。尽管有非正式的C字符的上面的语义基本上与有限模型中的形式语义是一样的。对于每个有限模型M=（DM，IM），状态和EPDL公式之间的有效性关系=M可以在μC公式上扩展如下：3. S|= M（µp.φ）i s |= Mφ i（false），其中i ≥ 0;4. S|= M（νp.φ）i s |= Mφ i（true），对于每个i ≥ 0。特别地，如果φ是一个公式，<$failmoveA（<$fail[moveB]（failwin））其中win是命题变量，那么公式WIN0就是假的。0赢得 （false），而WINi+1（i≥0）是φi+1（false）<$failA（<$fail[moveB]（failφi（false）。因此，以µC为单位，命题3.1可以重新表述如下：建议3.2Lett（P，M。A，M，B， F）是两个局中人和L的有限对策WIN是一个公式µ win。<$failmove A（<$fail [move B]（fail win））.• 对于每个i≥0，公式WINi（false）在以下状态下有效：G（P，MA，MB，F），其中参与人A有一个获胜策略，最多有i轮• 对于每个i>0，参与人A的每个i轮最多获胜策略的第一步包括移动到位置，在该，<$fail [移动B]（fail赢得• 一个公式WIN在G（P，MA，MB，F）的那些状态中是有效的，其中参与者A有一个获胜的策略• 公式WIN不等同于EPDL的任何公式6，分别读作φ希洛夫和伊41公司简介∩∅∩∅prog12用户4基于模型检测的元程序现在我们准备形式化一个参数化博弈GAME（N，M）。这个博弈中的位置是元组（U，L，H，V，Q），其中• U是[（M +1）.]中的一组硬币数。（M+N）]，目前正在讨论中，但没有对其他硬币进行测试;• L是[（M +1）.中的一组硬币数。（M+N）]，这些硬币目前正受到质疑，但与其他硬币进行了测试，结果变得更轻;• H是[（M +1）.中的一组硬币数。（M+N）]，这些硬币目前正受到质疑，但与其他硬币进行了测试，结果更重;• V是[1]中的一组硬币数。（N+M）]，目前已知有效;• Q是当前平衡查询，即 一对不相交的子集[1.. （N+M）]的相等基数。位置应满足以下列出的一些自然约束- ULH/=，既然有假币，- U、L、H和V构成[1.]的不相交覆盖。（N+M）]，- U= i <$L H=，因为一个错误是在未经测试的硬币中，即所有先前的平衡都给予了相等的权重，- 如果Q=（S1，S2），则要么S1 V=要么S2V= ，因为在天平的两个盘上添加额外的有效硬币是不合理的最终位置是位置（U，L，H，V，（N，N）），|U|+的|L|+的|H|= 1。玩家prog的可能移动是用于平衡两组硬币的查询即位置（U，L，H，V，（S，S））−→（U，L，H，V，（S1，S2））其中，S1和S2是[1.的不相交子集。（N+M）]，具有相等的基数。玩家用户的一个可能的移动是对引起位置改变的查询的回复，=或>（U，L，H，V，（S， S））−us→er（UJ，LJ，H J， VJ，（，））根据查询和回复，=或>。 我们不想为−→给出一个完整的（虽然简洁的）定义。 相反，我们想给它背后的一些直觉。 为此，让我们将S1表示为U1<$L1<$H1<$V1，将S2表示为U2<$L2<$H2<$V2，其中U1 ， 2<$U，L1 ，2<$L，H1，2<$H，V1，2<$V。 由于U i=i L H =，则有两种不相交的情况：U = XOR L H =。 让我们只考虑第一个，因为第二个是相似的。希洛夫和伊42∅21在这种情况下，U1=U2=UJ=，如果答案是，则为1，因为在这种情况下，<要么在L1中轻，要么在H2中重;LJ=如果回答是=，则返回（L\（L1<$L2）），因为在这种情况下，既不在L1也不在L2，既不在H1也不在H2;如果答案是>，则返回L，因为在这种情况下，要么在L2中轻，要么在H1中重;如果答案是，则为2，因为在这种情况下，<要么在L1中轻，要么在H2中重;HJ=如果回答是=，则返回（H\（H1<$H2）），因为在这种情况下，既不在L1也不在L2，既不在H1也不在H2;如果答案是>，则返回“”H“，因为在这种情况下，要么在L2中，要么更轻，要么在H1中，要么更重。在这里，一个游戏和相应的具体模型。模型检查[8]是一种针对公式测试模型的方法模型的逻辑正在考虑中的文件是过渡系统或Kripke结构，其中一个系统的状态是一个图形的节点，但状态之间的转换是作为标记的边缘。全局（模型）检查问题在于计算输入模型的所有状态的集合，其中输入公式是有效的，而局部（模型）检查在于测试输入模型的输入状态中的输入公式的有效性我们对有限模型的模型检测问题特别感兴趣对于这些模型，两个模型检验问题都是多项式等价的，所以我们不想在有限模型中区分它们更重要的主题是用于测量复杂性的参数。若M=（DM，（RM，PM））是有限模型，则设dM，rM和mM分别为DM中的态数，RM中的边数和（dM+rM）。如果模型M是隐式的，那么我们希望使用这些没有下标的参数，即。只有DRM如果φ是一个公式，那么让fφ作为字符串的φ的大小。如果公式φ是隐式的，那么我们希望使用这个参数fφ而不带下标，即只有f。最著名的模型检查算法的µ-微积分和有限模型是指数。例如，在一个示例中，O（m×f）×.mm×fa−1一是快速模型检查算法（FMC算法）[10]的时间界限，其中公式的交替深度a是交替的最大量希洛夫和伊43赢得赢得赢得¬ ∧∨∈在嵌套μ和ν关于句法依赖性和形式上是由归纳法定义的。我们想指出的是，对于每个公式，交替深度总是小于或等于定点的嵌套深度特别地，输入模型中的固定输入公式WIN的模型检查的复杂度在模型的大小上是线性的在模型检查方面，元语法问题的初步高级设计非常简单：(i) (a)输入整数N、M和K;(b) 设置玩家A为prog，玩家B为user;(c) 检查公式WINK在GAME（N，M）中;（d）如果（[（M +1）.. （M + N）]、N、N、[1.. M]，（λ，λ））|= GAME（N，M）WIN K，然后转到（ii），否则-输出不可能的策略并停止;(ii) 输出一个程序，它首先检查公式<$fail[moveB]（fail我赢 （false））对于i∈ [0. （K-1）]在博弈（N，M）中，然后有对于i [1.. K]向下：输出移动到一个位置其中公式失败[移动B]（失败WIN i-1（false））保持，输入<，=或>并根据它定义下一个位置。根据命题3.2，该设计是正确的。从纯数学的角度来看，具体的模型是相当不错的，并且实现了一个想法，即插即用上述初步设计似乎是自然的。对不起，从计算机科学的角度来看，具体的模型太大了，因为可能的位置和可能的移动量是N的指数函数。5通过抽象实现元程序现在，我们准备讨论一个新的抽象模型博弈（N，M）的参数化博弈（N，M）。如何解决元程序问题的提示很简单：考虑硬币的数量而不是硬币的数量。这个想法是自然的：当有人在解决难题时，他/她是根据不同种类的硬币的数量而不是根据它们的数量来操作的！博弈（N，M）中的位置是元组（u，l，h，v，q），其中• u是[1.]中的硬币数量。N]目前正在讨论中，但没有对其他硬币进行测试;• l是[1]中的硬币数量。N]目前正在讨论中，但与其他硬币进行了测试，结果变轻了;• h是[1.]中的硬币数量。N]目前正在讨论中，但与其他硬币进行了测试，结果更重;• v是[1]中的硬币数量。（N+M）]，目前已知有效;• q是平衡查询，即，一对四元组（（u1，l1，h1，v1），（u2，l2，h2，v2））的数字[1. （N+M）]。赢得希洛夫和伊44−→216五个约束与博弈（N，M）的约束密切相关：（1）u + l + h ≤ N，（2）u+ l + h + v = N + M，（3）u + l + h ≥ 1，（4）u/= 0 i/l + h = 0，（5）v1= 0或v2= 0. 应该对查询施加额外的但自然的约束（因为我们可以从可用的未经测试的，较轻的，较重的和有效的硬币中借用硬币进行称重）：（6）u1+ u2≤ u，（7）l1+ l2≤ l，（8）h1+ h2≤ h，（9）v1+v2≤v，（10）u1+ l1+ h1+ v1= u2+ l2+ h2+ v2。最终位置是位置（u，l，h，v，（（0，...，0），（0，..，0）），其中u + l + h = l。玩家prog的可能移动是用于平衡两组硬币的查询即位置prog（u，l，h，v，（（0，0，0，0），（0，0，0，0））（u，l，h，v，（（u1，l1，h1，v1），（u2，l2，h2，v2）.玩家用户的一个可能的移动是对引起位置改变的查询的回复，=或>（u，l，h，v，（（u， l， h， v），（u， l， h， v））−us→er1 1 112 222−us→er（uJ，lJ，hJ，vJ，（（0，0，0，0），（0，0，0，0）））根据询问和答复：如果回答是，，则返回0，n（l1+u1）如果回答是，<（l−（l1+l2））如果回复为=，(l+u)ifthereplyis>,2hJ=n（h2+u2）如果回答是，<（h−（h1+h2））如果回答为=，(h+u)ifthereplyis>,1VJ =（（N + M）−（uJ+ lJ+ hJ））。这样就形成了一个新的博弈和相应的抽象模型。在游戏（N，M）中的可能位置移动的总量小于（N+1）6。什么是抽象的效用？一般地，设Φ是一组公式，M1=（D1，I1）和M2=（D2，I2）是两个模型，g：D1→D2是一个映射.模型M2被称为模型M1关于公式Φi的抽象，对于每个公式φ∈ Φ和每个状态s∈D1，以下成立：|= 1φ g（s）|= 2φ。特别是，让我们考虑在这种情况下，7G被称为抽象映射希洛夫和伊45赢得赢得赢得|¬∧∨建立了博弈（N，M）和博弈（N，M）（N≥1，M≥0）的模型，并定义了一个计数映射计数：DGAME（N，M）→DGAME（N，M）如下：（1）（2）（3）（4）（5）（6）（|U|、|L|、|H|（q）其中q是（ （ |S1 双 U| 、 |S1L| 、 |S1 级 | 、 |S1-V| ） ， （ |S2 双 U| 、 |S2 双 排 | 、 |S2-H| 、 |S2-200V|））。这种计数映射可以在位置对上作分量扩展。简单来说，计数映射是一个标记图GAME（N，M）到另一个标记图GAME（N，M）上的同态，对于GAME（N，M）中的每个位置POS具有以下性质：count将在该位置开始/结束的玩家的所有移动映射到在count（POS）中开始/结束的游戏（N，M）中的同一玩家的移动这直接意味着一个模型博弈（N，M）是另一个模型博弈（N，M）的抽象，关于使用唯一的自由命题变量fail和两个动作变量moveuser和moveprog编写的μ-演算公式。现在我们准备修改一个初步的高级设计，并为元程序提供一个最终的高级设计的基于抽象的版本(i) (a)输入整数N、M和K;(b) 设置玩家A为prog，玩家B为user;(c) 检查公式WINK在博弈（N，M）中;（d）如果（N，0，0，M，（（0，...，0），（0，..，（0））|= game（N，M）WIN K，然后转到（ii），否则-输出不可能的策略并停止;(ii) 输出一个程序，它首先检查公式<$fail[moveB]（fail我赢 （false））对于i∈ [0. （K-1）]在博弈（N，M）中，然后有对于i ∈ [1.. K]向下：输出一个移动到一个 位置。这样count（POS）=game（N，M）fail[moveB]（failWINi−1（false）），输入，=或>并根据它定义下一个位置。最终高层次设计的正确性来自命题3.2，因为game（N，M）是GAME（N，M）的抽象6通过游戏测试模型跳棋在第2节中讨论的教授程序逻辑和模型检查的重要性是基于模型检查应用的重要性模型检测应用的主要领域是对作为有限状态系统的硬件和软件进行自动验证[8]。 新的应用领域包括高级软件规范的验证[4]自动测试生成[14]等。我们假设，在所有情况下，一个高层次的模型检查器的可靠性是极其重要的，由于模型检查的自动字符。赢得希洛夫和伊46但是，尽管验证工具的可靠性问题很重要，但只有在正式的验证社区中才有薄弱的举措。让我们讨论一些原因，这种情况的可靠性。首先，在自动演绎中，可靠性问题最有可能通过将证明者与证明检查器耦合来解决，使得证明者将被要求做出可以由证明检查器检查的证明这种方法似乎是合理的，因为它的简单性，因为证明相对于要验证的系统的大小来说是相对较短的，而证明检查具有线性复杂性。接下来，最流行的模型检查器SMV [5]和SPIN [16]是用于时态逻辑的模型检查器，即，它们只在元层面上使用定点，因此所有内部定点都独立于外部定点。在这种情况下，模型检查算法非常简单和透明[8]。不幸的是，上述两个原因对于有限模型中的µ- Calculus的模型检查器都是无效的由于模型检查“证明”的指数复杂性，“a la”定理证明方法是不可能的。同时，由于交替嵌套定点的复杂相互作用，时序逻辑的模型检查的自然透明性丧失了。因此，我们预见只有三种合理的方法来对有限模型中的微演算进行可靠的模型检查：• 同时多变量模型检查，• 对模型检查器进行初步的广泛测试，• 模型检查器的形式验证。由于上述复杂性原因，可靠模型检查的多变量方法是时间、空间和成本昂贵的。第二种方法似乎也有问题，因为测试生成本身就是一个不平凡的问题。下一段将简要讨论这个问题。就形式验证而言，让我们在最近的一篇论文中指出[22]，其中报告了从证明模型检查器自动生成 据我们所知，这是关于正式验证的模型检查器的第一篇也是唯一的论文。 这个经过验证的模型检查器是来自[26]的模型检查算法在Caml上的实现，它由交互式逻辑框架Coq从算法正确性的正式证明中生成。为什么在有限模型中对微演算的模型检查器进行广泛的测试是一个重要的问题？因为模型检查器的整体测试套装必须是透明的，必须有可预测的结果，同时应该利用固定点的非平凡组合但这两种主张是相互排斥的。对模型检查器进行全面测试的最合适的解决方案可能是在自动生成的测试集上对正式验证的模型检查器进行测试有限游戏的问题域似乎是手动全面测试模型检查器的最佳选择，因为它包括公式的可理解性在这种情况下，可以手动地或通过实现用于玩家模拟的程序机器人来检查正确性。希洛夫和伊47≥·•∈赢得下面我们展示了3个参数化有限游戏的例子，这些游戏用于在一个规范和验证项目REAL[18，19，20]中手动测试μ-Calculus和有限模型的模型检查器我们使用参数化游戏来跟踪模型检查器对模型大小的反应。第一个例子叫做游戏在两个玩家之间进行，Spoiler和Duplicator。位置是介于1和N之间的整数或故障（N）。Duplicator首先选择一个初始位置。然后Spoiler和Duplicator根据以下规则轮流移动：从位置i开始，下一个位置可以是i或i+ 10。一旦Spoiler移动到故障位置，复制方获胜，一旦Duplicator移动到故障位置，Spoiler获胜。问题：用复制器的获胜策略定义所有初始位置另一个例子是在新年前夕19NM（N，M [0.. 爱丽丝和鲍勃玩了千年游戏。游戏中的位置是19 NM-2000年的日期初始位置是从该时间间隔中随机选取的然后，爱丽丝和鲍勃依次采取行动：爱丽丝，鲍勃，爱丽丝，鲍勃，等等。对于Alice和Bob来说，可用的移动是相同的：如果当前位置是一个日期，那么下一个日历日期和下个月的同一天是可能的下一个位置。一个玩家赢得了比赛，他/她的对手是第一个启动2000年的人问题：用Alice的获胜策略定义所有初始第三个例子是第2节中描述的元程序问题这里我们要指出的是，上述所有例子都涉及公式WIN和WINi（false）对于i≥0。7结论本文介绍了一些非标准的模型检查经验，并讨论了如何定期教学，培训编程竞赛和验证工具的实施可以齐头并进，与模型检查和博弈论。同时，它也表达了作者的一种强烈信念，• 关于形式方法基础的主题，缺乏流行的讲座、教程和论文• 具有挑战性的程序设计问题是更好地教育和普及形式方法基础的好机会• 计算机科学期刊要大力推广形式化方法基础。希洛夫和伊48引用[1] 布 拉 德 · 菲 尔 德 ， 和 S. StirlingLocal Model Checking for Infinite StateSpaces，Theoretical Computer Science，96（1992），157-174.[2] Berezine S.A.，和N.V. ShilovAn approach to effective model-checking of real-timefinite-state machines in Mu-Calculus，Lecture Notes in Computer Science，813（1994），47-55.[3] 公牛队，和K. 《基本模态逻辑》，《哲学逻辑手册》，第二卷，Kluwer学术出版社，1994年（第1-88[4] Bultan T. ， R. Gerber 和 W. PughModel-Checking Concurrent Systems withUnboundedProbableVariables：SymbolicRepresentation，Approximation，and Experimental Results，ACM Trans. Lang.and Syst.，21（1999），747- 789.[5] 小伯奇E.M. Clarke，K.L. McMillan，D.L. Dill和L.J. HwangSymbolic ModelChecking：1020States and Beyond，Information and Computation，98（1992），142-170。[6] 伯 卡 特 岛 “Automatic Verification of Sequential Infinite-State Processes”,Lecture[7] Burkart O.，和B. Ste EscherenModel-Checking the Full Modal Mu-Calculusfor Infinite Sequential Processes，Lecture Notes in Computer Science，1256（1997），419-429.[8] 克拉克·EMO. Grumberg和D.Peled[9] 克里夫兰河基于表格的模型检验在命题μ演算，学报Informatica，27（1990），725-747。[10] 克 里 夫 兰 河 ， M. Klain 和 B.Mu 演 算 的 快 速 ， 计 算 机 科 学 讲 义 ， 663（1993），410-422。[11] 达姆·M L. Fredlund和D. GurovToward Parameter Verification of DistributedSystems，Lecture Notes in Computer Science，1536（1998），150- 185.[12] 艾默生公司，C.S. Jutla和A. P. Sistla关于Mu演算片段的模型检查，计算机科学讲义，697（1993），385-396。[13] 费金河，J.Y. Halpern，Y. 摩西和M. Y.《关于知识的推理》，麻省理工学院出版社，1995年[14] Gargantini A.，和G. Heitmeyer使用模型检查从需求规范生成测试，ACMSIGSOFT软件工程笔记，241999，146-162[15] 哈雷尔湾68，Springer-Verlag，1979年。希洛夫和伊49[16] Holzmann G.J.，和D. Peled：The State of Spin，Lecture Notes in ComputerScience，1102（1996），385-389.[17] 科 曾 湾 Results the Propositional Mu-Calculus ， Theoretical ComputerScience，27（1983），333-354.[18] Nepomniaschy V.A. ， 关 于 N.V.ShilovReal92 ： A combined specificationlanguage for systems and properties of real time communicating processes，Lecture Notes in Computer Science，735（1993），377-393.[19] NepomniaschyV.A.，N.V. Shilov和E.V. Bodin一种新的语言Basic-REAL，用于分布式系统模型的规范和验证，A.P.Ershovhttp://www.iis.nsk.su/bre/bre99/bre99ps.zip。[20] Nepomniaschy V.A.，N.V. Shilov和E.V. BodinSpecification and Verification ofDistributed System by means of Elementary-REAL language，Programmingand Computer Software，25（1999），222-232。[21] N.V.Shilov和 K. Yi，Program Logics Made Easy，韩国科学技术高级研究所&，ROPAS技术备忘录第2000-7号，URL：http://ropas.kaist.ac.kr/lib/doc/ShYi00.ps.gz。[22] 斯 普 伦 格 角 Coq 中 模 态 μ- 演 算 的 验 证 模 型 ， 计 算 机 科 学 讲 义 ， 1384（1998）167-183。[23] 史蒂文·P和C.StirlingPractical Mo