博士论文EU N I V E R S I T D F R A N C H E-C O M T对有效的基于模型的■阿洛伊斯·德·雷福斯博士论文EU N I V E R S I T D F R A N C H E-C O M T论文提交人芦荟DR EYFU S要获得弗朗什-孔泰大学博士学位专业：计算机科学对基于模型研究单位：FEMTO-ST光盘2014年 10月22日在评审团面前答辩：JacquesJULLIAND弗朗什-孔泰大学评审团主席教授Pierre-CyrilleHeaM博士生导师弗朗什-孔泰大学教授OlgaKoU chNAR eN ko 博士生导师弗朗什-孔泰大学教授IoannisPaRI ssIs皮埃尔·雷蒂格勒诺布尔INP教授报告员奥尔良大学HDR高级讲师报告员PascalP o I za T大学教授考试员。巴黎西南特拉德芳斯REM ER CIEM ENT SJ’aimerais 当我的士气和动力下降到这样一个地步，一个疯狂的想法认输有时使我疲惫的头脑，你知道该说什么和/或做什么，我非常感谢评审团成员，他们同意对然后，我要感谢我的父母皮埃尔特和劳伦特，以及我的姐姐范妮和弟弟乔奇，感谢他们永恒和无条件的支持。我很幸运有你，我永远不会告诉你我有多爱你。我还要感谢尼科和露露，感谢你们加入我们这个家庭以来给我们带来的幸福。我也要感谢那些帮助我坚持到最后的人，有时甚至没有意识到这一点。我特别想到的是Cyber、Tcharlz、Nesnours、@ngel、Fouad、Oscar、Aydeé、Richard、Justine、Lysiane和Anne-Sorya。我不想忘记感谢我在第戎的减压阀：Cyber、Anne-Sophie、Chloé、Féfé和Jean-Marc，感谢你们的热情好客、我们的热情和我们的讨论，当我情绪低落的时候，这对然后卡卢、杰罗姆、奥斯卡、塞布、马蒂亚斯、罗密欧、克尔库埃特、塞库、亚历山德鲁、朱利安、莱昂内尔、伊万、尤苏、贝蒂、尼古拉斯、让-玛丽、福阿德、亚历山大、文森特·H.、拉米、约翰、纪尧姆、莱米亚、大卫、瓦莱丽、奈玛、帕科、萨尔加、阿尔班、艾德、扬博、雷吉斯、拉米尔、埃琳娜和亚历山大，因为他们我祝愿那些现在正在划船的人好运和顺风。还有那么多人（朋友、堂兄弟姐妹、同事）。. .）我真的很感激他们，他们值得我感谢，很明显，我不可能详尽无遗所以我的祖母我 简介151序言171.1背景。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...171.2捐款。 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ...181.3计划。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...181.4出版物。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...182理论基础和符号212.1自动机和常规语言。 . . . . . . . . . . . . . . . . . . . . . . . . .212.1.1词汇和语言。 . . . . . . . . . . . . . . . . . . . . . . . . . . . . ...212.1.2有限自动机和正则表达式 . . . . . . . . . . . . . . . .212.1.3自动机产品 . . . . . . . . . . . . . . . . . . . . . . . . . . . ...232.1.4自动机的同构。 . . . . . . . . . . . . . . . . . . . . . . . ...232.1.5自动机的简化。 . . . . . . . . . . . . . . . . . . . . . . . . ...242.1.6完成的字母到字母传感器。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...262.1.7将传感器应用于PLC. . . . . . . . . . . . . . . . ...272.1.8将转换器应用于语言。 . . . . . . . . . . . . . . . . ...282.2代数语法和堆栈自动机。 . . . . . . . . . . . . . . . . . . ...282.1代数语法。 . . . . . . . . . . . . . . . . . . . . . . . . ...282.2.2电池供电的自动机。 . . . . . . . . . . . . . . . . . . . . . . . . . . . . ...292.2.3语法中派生树的均匀随机生成312.2.4... ... ... ... ... ... ... ... ... ... ... ... ... ... ...33II可达性分析的正则近似353背景和问题393.1问题的介绍和陈述。 . . . . . . . . . . . . . . . . . . . . . . ...39总结83.2建议的技术。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...423.3超近似值的计算。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...43我的祖母3.4近似值的无穷大n4贡献：句法融合标准4.1进出494.2左和右504.3近似函数的组合4.4实验534.5结论545贡献：使用换能器状态的近似函数5.1其他定义555.2使用换能器状态的融合标准585.3使用换能器61的状态的近似5.4实验645.5结论666第二部分的结论III结合随机生成和覆盖标准，从7背景和问题737.1软件测试737.1.1自动测试737.1.2基于模型的测试（MBT）747.1.3覆盖范围标准747.1.4随机测试757.1.5有限图中路径的随机一致生成7.1.6从电池型号76开始7.2我们在哪里？......................................................................................................................777.2.1随机生成路径与随机路径777.2.2结合随机生成和覆盖标准787.2.3正则模型（无堆栈）与代数模型（有堆栈）807.2.4贡献：结合随机生成和覆盖标准在电池82总结88贡献：应用于语法83摘要98.1计算pX， n和 pX， Y， n.......................................................................................................................................848.2正在计算|E X，n（G）|和|E X、Y、n（G）|.....................................................................848.3实验879贡献：在电池供电自动机上的应用9.1一致FDA-Trace的随机均匀生成939.1.1一致迹线的随机生成939.2PDA 94的覆盖范围标准9.2.1所有州........................................................................................................的标准949.2.2所有过渡的....................................................................................................标准959.2.3结合随机试验和覆盖标准979.3实验979.3.1技术信息989.3.2说明性示例989.3.3覆盖范围标准的说明性示例1019.3.4超过103个示例的运行时间9.4案例研究9.4.1描述1069.4.2用于分流场算法的底层自动机9.4.3实验1099.5讨论10910 第三部分的结论四、结论和展望11711 结论和展望119我的祖母前前TABL E 从 FI G是2.1Aex（自动机示例2.2Aex2（自动机的第二个示例2.3A1× A2.......................................................................................................................... 232.4Aex× Aex2........................................................................................................................................................242.5同构自动机242.6Aex/~................................................................................................................................................................................... 252.7T（A1）/~exe...............................................................................................................................................................................................................252.8在（Aex）26中2.9Tex（传感器示例）262.10 Tex（Aex）272.11T（A1）282.12 令牌环282.13 对应于序列S、 aS b、 aTbb、 abb................................................................................. 29的派生树2.14 A电源，NPDA 302.15 随机生成算法322.16 生成一致FDA-traces的语法示例3.1过近似法423.2连续过近似433.3C右（A）44的计算3.4半固定点算法443.5令牌环：F=Left45的PointFixe半算法3.6需要对近似值进行微调的情况3.7算法向后............................................................................................ 分析463.8第47章第一次见面4.1在（Aex）504.2输出（Aex）504.3在F T，2............................................................................................................................................................514.4在右边，3. ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...51TT4.5左（Atr1）524.6右（Aex）524.7使用语法标准的结果545.1x·Aex..................................................................................................................................................................................... 565.2Aex3...................................................................................................................................................................................... 565.3Aex4...................................................................................................................................................................................... 565.4令牌环：将传感器T应用于QC×Q*-自动机（1）575.5令牌环：将传感器T应用于QC×Q*-自动机（2）585.6令牌环：基于传感器状态的合并（1）595.7令牌环：基于传感器状态的合并（2）595.8PointFixeT61的半算法5.9需要对近似值进行微调的情况5.10 算法分离635.11 算法细化器....................................................................................................635.12 分离和细化....................................................................................................算法的示例635.13 改进后的验证半算法645.14 C 65自动机的类型5.15 使用基于换能器状态的方法作为融合标准的结果667.1不同类型测试的分类747.2有限图示例757.3例1 777.4示例2 787.5随机生成-算法1 797.6随机生成-算法2 797.7随机生成-算法3 807.8概率πe的计算，以.............................................................................................................7.9C语言程序，计算xn...........................................................................................................................................817.10 xn..................................................................................................................................................................................... 81的控制流程图8.1示例8.3中语法G的派生树8.2示例8.3中GX语法的派生树9.1程序的随机测试方法9.2一致迹线的随机生成93图表12exeexe表139.3A6的底层自动机. . . . . . . . . . . . . . . . . . . . . . . . . ... ...959.4A（6，h， 9）的基本自动机. . . . . . . . . . . . . . . . . . . . . . . . ... ...969.5计算πq概率，以......................................................................................................................9.6相互递归函数989.7模：例99中的9.8自动机Axpath..........................................................................................................................................................1019.9分流场算法1079.10 用于分流场算法的底层自动机9.11 分流场算法的C语言实现1109.12 分流场算法的C实现，我们在2 / 2中测试了该算法111我我不知道你是谁1PRoL ogU e1.1CoNT exT e开发安全、可靠和无错误的程序是现代计算机科学中最困难的软件在我们的日常生活中无处不在，我们委托它们执行越来越敏感的任务，比如在网上订购时传输我们的银行数据当故障的后果可能特别严重时，例如当生命或大量资金（数百万/数十亿欧元）处于危险之中时，我们谈论的是关键软件例如，这涉及用于运输系统（飞机、火车、汽车等）的软件。... （）、 ... （）、健康（医院管理、医疗器械、... （）、金融（证券交易所、在线或信用卡支付、... （）、或者在军事领域（导弹、无人机、加密通信等）。... .）在航空航天领域... （.）因此，能够确保这些软件的质量是必不可少的在这种情况下，我们可以区分两种互补的技术来评估计算机系统的质量验证是从数学上证明它可以用一个支持性的证明（例如Coq）来完成，帮助工程师构建形式化的验证也可以通过模型求解来完成，通常使用的术语是模型检查，这是一种试图根据系统的模型来检查其所有可达到状态是否满足（或不满足）性质的验证的主要缺点之一是现有技术的算法复杂性，这使得它们非常适用于大规模系统与验证不同，测试不提供正式的上游证据但是测试技术可以应用于大型系统，并且在实践中与高质量软件的开发测试在软件开发中扮演着越来越重要的角色，以至于开发了测试驱动开发（简称TDD）的方法，该方法主张在在过去的十年中，为了应对测试阶段日益增长的重要性，已经进行了大量的工作，目的是1.2CoNTRIBUTI oN s本文对基于模型的验证与确认做出了贡献我们在验证方面的贡献是定义了两种新的常规模型检查近似技术计算所有可达状态的过近似 第一种技术是根据简单的语法标准或这些标准的组合，通过合并自动机的状态来过度近似所有可达状态（参见：第4节）。第二种近似技术也包括合并自动机的状态，但这次使用换能器（参见第5.2节）。 此外，对于第二种技术，我们开发了一种新的近似方法（参见第5.3节），受CEGAR范式的启发（参见第3.4节）。这两种用于常规模型检查的近似技术对于测试，我们的贡献是定义了一种技术，该技术允许将随机生成与覆盖标准相结合，使用代数语法或堆栈自动机在[DGG+ 12]中，解释了如何使用由覆盖准则给出的约束来偏置有限图中的均匀随机检验方法，以最大化但是有限图通常表示被测系统的强抽象，因此存在许多抽象测试无法实现（我们已经扩展了这种方法，将其应用于代数模型（第8章中的代数语法和第9章中的堆栈自动机），这降低了模型的抽象程度，从而减少了我们将随机生成与代数语法的覆盖准则相结合的技术1.3PLAN在第二章中，我们介绍了阅读本论文所必需的所有定义、符号、命题和定理。我们首先介绍第二部分介绍了我们在验证领域的贡献：第三章介绍了常规模型检查和近似的建立在第4章中，我们提出了一种用于常规模型检查的技术，该技术包括根据简单的语法标准或这些标准的组合，通过合并自动机的状态来过度近似所有第5章介绍了一种使用新的合并标准的技术，该标准利用了系统的转换关系。第三部分介绍了我们在测试领域的贡献：第7章介绍了我们工作的背景。然后，我们在语法（第8章）和堆栈自动机（第9章）中将随机生成与覆盖标准相结合。第一部分第一章第一次见面序言18第一部分第一章第一次见面第十九章1.4/PUBLIcaTI oN s本论文以已发表的著作为基础。以下是我参与的项目列表[DHK13a]包含两种常规模型检查方法：第一种方法使用可以与逻辑运算符组合的语法标准（参见第四章），第二个利用系统的过渡关系（cf. 第五章[DHK13b]描述了我们在语法测试中将随机生成与覆盖率标准相结合的方法（参见第八章[DHKM14]详细介绍了如何将随机生成与覆盖标准相结合，从堆栈自动机开始（参见第九章
我的内容管理
展开
