没有合适的资源?快使用搜索试试~ 我知道了~
警告:警告链接这份文件是长期工作的结果,得到了答辩小组的批准,并提供给整个更广泛的大学社区。它受作者的知识产权保护。 这意味着在使用本文件时有义务引用和引用另一方面,任何伪造、剽窃、非法复制的行为都将受到刑事起诉。联系方式:ddoc-theses-contact@univ-lorraine.fr知识产权法。第122条。4知识产权法。条款L 335.2- L335.10http://www.cfcopies.com/V2/leg/leg_droi.phphttp://www.culture.gouv.fr/culture/infos-pratiques/droits/protection.htmIAEM洛林DFD计算机科学博士学校- ----------------------------------用于基于事件的B规范验证的仿真环境论文于2013年11月29日提交并公开支持洛林大学博士学位(Sp专业:计算机科学)通过法清和昂报告员:陪审团组成Michael LEuschel德国杜塞尔多夫大学教授Catherine DUBOIS埃夫里ENSIIE教授检查员:Pascale LE GALL巴黎中央学院教授Stephan MERZINRIA研究主任,南希论文主任:Jeanine SOuquières洛林大学教授,南希,LORIA Jean-PierreJACQUOT洛林大学讲师,南希和洛丽亚- ----------------------------------UMR 7503洛林计算机科学及其应用研究确认文件- ----------------------------------首先,我想向我的顾问Jeanine Souquières教授和我的共同顾问Dr.Jean-PierreJacquot博士期间的持续支持学习和研究,为他们的耐心,动机,热情,和巨大的知识。没有他们的指导,我无法想象成功地实现我的研究目标。我也想感谢他们在我生活中的帮助,尤其是在国外。我将永远记住他们是最好的顾问和终身导师。此外,我还要感谢我的论文委员会的其余成员:Michael Leuschel教授,教授。凯瑟琳·杜波依斯教授帕斯卡尔·勒·加尔博士Stephan Merz,感谢他们的参与、深刻的评论和建设性的批评。此外,我还要感谢LORIA的MAIA和TRIO团队的同事,特别感谢Alexis Scheuer博士开发了2D队列数学模型。我想特别把这篇论文献给我的家人,感谢他们的爱、支持、耐心和理解。他们允许我把大部分时间花在这篇论文上。最后,但肯定不是最不重要的,我感谢我的朋友们,感谢他们所有的精神鼓励和支持。内容1简介11.1动机。 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ...11.1.1研究背景。 . . . . . . . . . . . . . . . . . . . . . . . ...11.1.2科学问题 . . . . . . . . . . . . . . . . . . . . . . . ...21.3技术问题。 . . . . . . . . . . . . . . . . . . . . . . ...21.1.4目标。 . . . . . . . . . . . . . . . . . . . . . . . . . . . ...31.2贡献 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ...31.3案例研究。 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ...41.4出版物。 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .41.5论文大纲。 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ...62最新技术水平72.1引言。 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .72.2开发过程。 . . . . . . . . . . . . . . . . . . . . . . . . . ...82.2.1施工活动。 . . . . . . . . . . . . . . . . . . . . ...92.2.2验证和确认活动。 . . . . . . . . . . . . .102.2.3其他活动。 . . . . . . . . . . . . . . . . . . . . . . . . ...112.2.4一些过程模型。 . . . . . . . . . . . . . . . . . . . . ...112.3形式方法。 . . . . . . . . . . . . . . . . . . . . . . . . . . . . ...132.3.1正式规范。 . . . . . . . . . . . . . . . . . . . . . ...132.3.2正式验证。 . . . . . . . . . . . . . . . . . . . . . . ...142.3.3代码生成 . . . . . . . . . . . . . . . . . . . . . . . . ...142.4B方法142.4.1概述142.4.2活动演示文稿152.4.3罗丹平台182.5事件B模型的动画202.5.1动画难度202.5.2事件B动画师202.5.3细化22的多级别动画2.623排模型2.6.1排长队问题232.6.21D排队模型242.6.32D队列模型252.7摘要27我ii内容I事件B可用性2931D排式模型31的分析3.1导言313.2证据323.2.1交互式证明323.2.2错误陈述333.2.3无法证明的目标343.3无冲突属性363.3.1机器排0363.3.2机器排1373.3.3机器排2373.3.4第3排和第4排383.4摘要384DLF定理的自动生成4.1导言394.2死锁自由规则404.2.1完全40型的锁锁自由度4.2.2事件子集的死锁自由度4.3工具要求414.4第42期实施4.5使用424.6摘要435使用Event-B45进行扩展5.1导言455.2模型结构465.2.1事件的分解465.2.2复杂性增加485.3物理和数学方程485.3.11D方程拟合485.3.22D方程拟合495.4时间属性505.5工具的调整515.5.1第52版5.5.2验证525.5.3验证525.6摘要53IIEvent-B55的JavaScript模拟框架6JEB设计576.1导言576.2模拟生成器的要求586.3仿真框架60的体系结构内容III6.4实施选择616.5翻译策略626.5.1注释与 设置库.................................................................................626.5.2用户手动编码功能的636.5.3变量、见证和变量636.5.4定量公式646.6摘要647JEB实施657.1导言667.2命名空间667.3语境的翻译677.3.1集合和常量687.3.2公理687.3.3常数检查器687.4机器的翻译687.4.1变量697.4.2不变量707.4.3事件707.4.4事件参数717.4.5事件警卫727.4.6事件操作737.4.7用户界面747.5公式75的翻译7.5.1预测值757.5.2表达式767.5.3任务787.6翻译公式的解释797.7模拟控制797.7.1模拟调度程序797.7.2模拟的参数807.7.3场景控制器807.7.4动画师807.8事件B项目图817.9摘要818JeB模拟的利用和分析838.1引言。 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .838.2 1D排的模拟 . . . . . . . . . . . . . . . . . . . . ...848.2.1最小模拟. . . . . . . . . . . . . . . . . . . . . . ...848.2图形显示。 . . . . . . . . . . . . . . . . . . . . . . . ...868.2.3细化的模拟。 . . . . . . . . . . . . . . . . ...868.3 2D队列模拟 . . . . . . . . . . . . . . . . . . . . ...868.1载波集。 . . . . . . . . . . . . . . . . . . . . . . . . . . ...878.3.2由属性定义的函数。 . . . . . . . . . . . . . . . ...888.3.3参数的生成和常量的定义。 . . . . ...89iv内容8.4对JeB使用的898.4.1模拟成本898.4.21D排式模型898.4.32D排式模型908.4.4传输域模型918.4.5MIDAS91型8.4.6现有动画师之间的比较8.5从验证角度进行分析948.5.1公理94的验证8.5.2属性的验证958.6摘要969模拟的正确性979.1导言979.2一致的行为989.2.1事件-B机器的语义9.2.2事件-B机器的操作解释9.2.3模拟器的执行1009.2.4模拟的正确性1019.2.5义务证明1029.3关于假设的1049.3.1假设11049.3.2假设21059.3.3假设31059.4摘要10510 结论和未来工作10710.1 结论10710.2 未来工作10810.2.1 技术10810.2.2 Event-B108的细化过程10.2.3 方法110附录113附录A论文用法语发表113附录B事件-B公式125的翻译附录C Event-B 149的JavaScript库附录DEvent-B 183中的1D队列模型附录EEvent-B 199中的2D队列模型参考书目251图列表2.1主要开发活动 . . . . . . . . . . . . . . . . . . . . . . ...92.21D队列模型 . . . . . . . . . . . . . . . . . . . . . . . . . . ...242.32D队列模型 . . . . . . . . . . . . . . . . . . . . . . . . . . ...263.1机器排2的DLF定理 . . . . . . . . . . . . . . ...353.2机器排中无法证明的目标。 . . . . . . . . . . . . ...364.1DLF定理的生成器。 . . . . . . . . . . . . . . . . . . . . . . ...435.1排队模型的结构。 . . . . . . . . . . . . . . . . . . ...476.1JeB仿真框架 . . . . . . . . . . . . . . . . . . . . . . . ...607.1持续检查器 . . . . . . . . . . . . . . . . . . . . . . . . . . . . ...697.2机器用户界面 . . . . . . . . . . . . . . . . . . . . . . . . ...747.3事件-B项目图 . . . . . . . . . . . . . . . . . . . . . . ...818.1事件B中点的定义 . . . . . . . . . . . . . . . . . . . ...8710.1 事件-B的再优化步骤。 . . . . . . . . . . . . . . . . . . . ...10910.2 扩展的V型。 . . . . . . . . . . . . . . . . . . . . . . . . . ...111A.1L’architecture de JeB . . . . . . . . . . . . . . . . . . . . . . . . . ...119Vvi图列表表列表4.1DLF定理大小414.2回顾的1D队列模型43中的死锁自由5.11D模型47中移动事件的分解5.22D模型47中运动事件的分解5.3复杂性增加486.1模拟生成器的要求597.1模拟器代码67中使用的命名空间7.2上下文的结构映射677.3机器的结构映射7.4事件的结构映射708.11D队列模拟的878.2模拟成本898.3现有动画师之间的技术比较8.4在我们的案例研究中使用四个动画师9.1符号和符号98七八、表格列表第一章简介内容1.1动机11.1.1研究背景11.1.2科学问题21.1.3技术问题21.1.4目标31.2贡献31.3案例研究41.4出版物41.5论文大纲61.1动机1.1.1研究背景系统开发的经典方法是通过人类活动进行不幸的是,人类经常犯错误和失误是潜在的安全威胁情况的最常见原因。例如,阿丽亚娜5号火箭1号的第一次试飞于1996年6月4日因控制软件故障而失败。从64位浮点值到16位有符号整数值的数据转换未被工程师检查;它产生了导致火箭破坏系统的质量可以通过减少开发过程中的人为错误来提高,例如,通过对整个系统或一些关键子系统使用形式化方法。形式化方法使用数学逻辑来抽象地表示系统,证明形式化规范与需求一致,证明实现满足规范,并从规范生成代码。1. http://en.wikipedia.org/wiki/Ariane_512第1章. 引言在本文中,如果一个系统满足以下两个条件,则称其为正确的– 验证:系统必须内部一致,并且必须符合初始规范,即我们正在正确地构建它。验证活动通常是由开发人员执行的内部过程。– 已验证:系统必须满足其用户的预期用途,即我们正在建造正确的东西。验证活动需要涉及开发人员以外的人员(利益相关者)的过程。使用形式化方法,获得经过验证的规范相当容易。但是,经过验证的规范不会自动生成经过验证的规范。验证和确认是独立的程序。它们应一起使用,以确保正式规范的正确性。通常,验证活动是通过数学证明进行的,需要大量的资源(时间、金钱和经验)。这使得形式化方法更适合于故障成本非常高的安全关键系统的开发例如,在铁路或航空航天领域,未检测到的错误可能导致生命损失。本文主要研究安全关键系统的规范、验证和确认,我们的研究工作从分析现有的Event-B规范开始,该规范通过排队算法将纵向控制形式化在排队模型中必须保持的安全特性是车辆之间没有碰撞然后,我们通过添加横向控制将此正式规范扩展到二维。1.1.2科学问题我们研究工作中使用的案例研究未涵盖的最重要科学问题是:正式规范的数学证明不足以保证其正确性:验证不等于验证。基于证据和基于再融资的开发技术保证了开发在形式意义上是内部一致的。特别地,这些技术保证在开发期间编写的所有模型满足初始正式规范。然而,非功能性需求通常很难在标准逻辑中表达;许多需求甚至在这样的数学框架之外。Hence,它们不在最初的规格中。此外,在开发的早期阶段获得清晰和完整的要求被认为是一项几乎不可能完成的因此,初始要求文件可能不完整、不明确、不一致。因此,开发人员将不得不"提供"缺失的需求,以便在工作过程中做出必要的决策。因此,应在正式模型经过验证后尽快对正式模型执行验证活动。1.1.3技术问题使用Event-B开发系统会带来一些技术问题:1.2. 捐款3– 缺乏支持验证活动的实用工具– 缺乏将正式和半正式推理整合到开发过程中的指南。1.1.4目标我们的工作重点是与扩展Event-B可用性相关的具体目标:1. 最重要的目标是建立一个可以模拟Event- B模型进行验证的框架。该框架允许我们保证模拟的语义正确性。该框架是对现有验证和动画工具的补充,这些工具允许将验证活动与再融资链上的验证活动相关联2. 第二个目标是帮助验证Event-B模型中是否存在死锁。3. 最后一个更符合方法论的目标是思考和扩展Event-B中使用的再融资的核心符号。最先进的改进重新强调了验证活动。我们通过其他活动来补充它,如需求管理、数学模型的调整、时间属性的检查以及通过动画或模拟的验证。1.2贡献在这篇论文中,我们试图定义两个重要的贡献。贡献I:Event-B可用性我们研究工作的起点是评估Event-B的可用性:– 对最初的1D队列规范进行批判性分析,并解释行为中的一些异常,– 一个罗丹插件(Java中大约500行),用于自动生成无锁定理,– 从不同方面(数学、结构、时间属性和工具)对Event-B的可扩展性进行评估贡献2:Event-B的JavaScript模拟框架我们的主要贡献是基于JavaScript的Event-B模拟框架该框架从Event-B模型生成模拟器,并提供轻量级图形执行环境。模拟器可用于在每个再制造步骤验证Event-B模型。它们帮助最终用户、领域专家和开发人员更好地理解数学模型和规范。该模拟框架包括:4第1章. 引言– Event-B模型的集成仿真环境,由两个主要元素组成:– 一个翻译器(Java中约2800行):一个罗丹插件,它自动生成Event-B模型的模拟器,以及– 一个运行时环境和最著名的JavaScript库(JavaScript中大约2700行),支持所有Event-B数学表示法,– 基于证明义务生成的模拟正确性语义。1.3案例研究我们在研究工作中使用了四个案例研究这些案例研究使我们能够尝试转换Event-B模型、实现模拟器和参数化模拟的不同策略。目前,这些模型的所有重新设计都可以通过我们的工具进行模拟。该模型[Lanoix 2008]旨在使用Event-B验证一维排队算法它包含10个组件和大约600行Event-B正式文本。它可以由现有的Event-B动画师使用一些策略来动画化亨斯,我们用它作为参考。该模型[Yang 2011]是第一个二维模型的扩展。它包含10个组件和大约1800行Event-B正式文本。它有一个抽象载体集和一些无法解释的函数,导致现有的Event-B动画器失败亨斯,我们把它当试验床用。此模型[Mashkoor 2009 a]将Event-B中它包含23个组件和大约1100行Event-B正式文本。它使用许多Event-B数学符号,例如,抽象载体集、集合理解、非确定性赋值。我们使用此模型来测试Event-B库的接口和符号执行。MIDAS模型此模型[Wright 2009 b,Wright 2010]使用Event-B来构建指令集架构。它包含104个组件和大约21,800行Event- B正式文本。它有一个复杂的上下文结构,以及由40台机器组成的最长的抽象机再生成链我们用它来测试JeB在大型项目中的可扩展性。1.4出版物本文获得的结果已发表在以下论文中:1.4. 出版物5国际会议[1] 杨法清、让-皮埃尔·雅库特和珍妮·苏奎耶尔。测试Event-B模型模拟的保真度2014年在美国迈阿密举行的第15届IEEE高保证系统工程(HASE)国际研讨会上[2] 杨法清、让-皮埃尔·雅库特和珍妮·苏奎耶尔。JEB:JavaScript中Event-B模型在第20届亚太软件工程大会(APSEC)上,泰国曼谷,2013年。[3] 杨法清、让-皮埃尔·雅库特和珍妮·苏奎耶尔。使用模拟验证Event-B规范的案例。在第19届亚太软件工程大会(APSEC)上,中国香港,2012年[4] 杨法清和让-皮埃尔·雅库特。使用Event-B进行扩展:案例研究。见MihaelaBobaru、Klaus Havelund、Gerard Holzmann和Rajeev Joshi,编辑,NASA形式方法(NFM),计算机科学讲座笔记第6617卷,第438-452页施普林格柏林/海德堡,2011年。[5] 杨法清和让-皮埃尔·雅库特。用于创建Deadlock- Freeness定理的Event-B插件在第14届巴西形式方法研讨会(SBMF)上,巴西圣保罗,2011年全国会议[6] 杨法清和让-皮埃尔·雅库特。JeB:事件驱动B的JavaScript模拟环境。《软件开发援助的形式化方法》[7] 杨法清、让-皮埃尔·雅库特和珍妮·苏奎耶尔。将基于事件的B转换为C,以便通过模拟进行验证。《软件开发援助的形式化方法》[8] 杨法清和让-皮埃尔·雅库特。证明?然后呢?《软件开发援助的形式化方法》研讨会文章摘要[9] 杨法清和让-皮埃尔·雅库特。从Event-B规范生成可执行模拟。在罗丹用户和开发人员研讨会上,枫丹白露,法国,2012[10] 杨法清和让-皮埃尔·雅库特。用于创建Deadlock- Freeness定理的Event-B插件在罗丹用户和开发人员研讨会上,枫丹白露,法国,2012[11] Atif Mashkoor、杨法庆和让-皮埃尔·雅库特。正式规范的验证:动画的案例第三届安全性和可靠性研讨会,德国特里尔,2011年。
下载后可阅读完整内容,剩余1页未读,立即下载
![doc](https://img-home.csdnimg.cn/images/20210720083327.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)
![](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://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- 共轴极紫外投影光刻物镜设计研究
- 基于GIS的通信管线管理系统构建与音视频编解码技术应用
- 单站被动目标跟踪算法:空频域信息下的深度研究与进展
- 构建通信企业工程项目的项目管理成熟度模型:理论与应用
- 基于控制理论的主动队列管理算法与稳定性分析
- 谷歌文件系统下的实用网络编码技术在分布式存储中的应用
- CMOS图像传感器快门特性与运动物体测量研究
- 深孔采矿研究:3D数据库在采场损失与稳定性控制中的应用
- 《洛神赋图》图像研究:明清以来的艺术价值与历史意义
- 故宫藏《洛神赋图》图像研究:明清艺术价值与审美的飞跃
- 分布式视频编码:无反馈通道算法与复杂运动场景优化
- 混沌信号的研究:产生、处理与通信系统应用
- 基于累加器的DSP数据通路内建自测试技术研究
- 跨国媒体对南亚农村社会的影响:以斯里兰卡案例的社会学分析
- 散单元法与CFD结合模拟气力输送研究
- 基于粒化机理的粗糙特征选择算法:海量数据高效处理研究
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](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)