Rodin基本操作

Rodin基于Eclipse开发，所以基本操作和Eclipse差不多

新建工程

填写项目名称

新建Event-B组件

组件类型有Context（上下文）和Machine（机器），组件名字随便起，不过后面会有精化操作，可以从0开始编号

Rodin中添加元素一般都是通过右键添加，直接写代码的方式有是有的，不过要装插件

添加完成后，可以双击元素，修改名称，其他的定义初始化相关操作也都是这样子添加

">"这个后面代表的是注释，双击这个符号的右边就可以添加注释了

右下角有个符号表，有什么需要输入的符号可以从这里找，把鼠标悬停到这里也可以看到快捷输入方式

例如:∅\varnothing∅直接输入{}就可以出来，∈\in∈直接敲:，→\rightarrow→敲–>，等等等等

在左上方有添加变量的快捷方式

右上方这里有切换视图的地方，使用插件或者查看验证的时候需要在这里切换视图观看

Event-B一个重要的特点就是精化，在组件上右键，context有extend操作，而在machine上有refine操作

左边explorer里面点开Proof Obligations可以看到Rodin自动生成的证明义务，通过的是绿色的，而未证明通过的是红色的，可以双击进去看看未通过原因

另：有时候可能你是对的，但平台没有证出来，这种时候可以双击进去看看原因，如果没啥问题可以右键Retry Auto Provers一下，有时候就直接绿了（微笑(*￣︶￣)）

看到这个not theorem了没有？这点下会变成theorem（定理），代表这一行内容目前并不能确定，需要在本组件内证明，所以不要乱点后面灰色的部分

同样，如果一个事件继承了另一个事件，那么点击not extended ordinary会变成extended，然后出现被继承事件的内容

Event-B表示法

机器和上下文

Event-B模型里面包含机器(machine)和上下文(context)，分别代表着模型中动态变化的部分以及静态不变的部分

机器和上下文之间的关系

机器和上下文之间存在着各种关系

一部机器可以“观看(see)”一个上下文
机器可以"精化(refine)"至多一部机器
一个上下文可以"继承(extend)"若干上下文

上下文的结构

一个上下文要有一个唯一的名字
extend列出当前上下文继承的上下文
sets定义一些不相交的集合
constants列出上下文的各种常量
axioms列出常量需要服从的各种谓词，也就是公理
theorems列出各种定理，它们必须在这个上下文的范围里证明

一个具体上下文的例子

机器的结构

一部机器有一个唯一的名字
refines包含被该机器精化的机器
sees列出本机器显示观看的上下文
variables列出机器的各种变量
invariants列出变量必须服从的各种谓词（即不变式）
theorems列出各种定理，需要在本机器中证明
variant描述变动式
events列出本机器的各种事件

一部具体的机器

事件

refines列出该事件精化的抽象事件
any列出事件的参数
where包含事件的各种guard
with是结合refines一起用的，在抽象事件里面的抽象参数，如果在具体事件里面有了具体的值，那么就在with语句中写出，定义使用a:P(a)的形式
then列出事件各种动作

with的使用

事件的例子

证明义务

1、不变式证明义务：INV

不变式证明义务规则保证machine里面的每一个不变式，在每个事件执行后仍然得到保持

该PO的命名为"evt / inv / INV"

2、卫加强证明义务：GRD

我们认为，正确的精化时，需要保证具体的卫比抽象的卫更强，什么叫更强？这就意味着具体的卫蕴含着抽象的卫，也可以说不可能出现一种情况，使得具体的卫成立，但抽象的卫不成立。正确精化的证明义务用GRD表示。

该PO的命名为"evt / grd / GRD"

变动式相关的证明义务
当引进了一些新事件时，我们还必须证明另外一些东西，就是说它们不会发散，也就是说，这些新事件不会永无止境地执行。为了证明这一性质，我们必须给出一个自然数值的表达式，称为变动式(variant)，而后证明所有的新事件都会减少它的值。这就带来了两个证明义务：第一个是说我们提出的这个变动式是一个自然数，第二个是说每个新事件都会减小该变动式的值

3、数值变动式证明义务：NAT
该证明义务保证，我们提出的变动式是一个自然数

4、变动量证明义务：VAR
该证明义务保证，我们提出的变动式在执行所有的新事件后都会减少它的值，

其实提出的这个变动式相当于while循环中的那个条件，我们如何确认while循环会终止呢？假设while循环长成while(n>0)这个样子，我们要确保n每次都会减小就行了，而我们提出的变动式需要在新的事件执行后，这个变动式会确实的减少，从而表明新的事件不会永无止境的运行下去，不然的话，新增的事件有可能导致本来的事件不会执行，这就违反了精化的原则

5、定理证明义务：THM
这一规则保证所提出的上下文或及其定理是可证的

该PO的命名为"thm / THM"

6、良好定义证明义务：WD
这一证明义务保证，每个可能出现病态定义的公理、定义、不变式、卫、动作、变动式，都确实是良好定义的

弄清楚一个问题就可以，什么叫做病态定义？如果我们把一个数定义为a = 1/0，这个就是一个病态定义，因为除法不能除以0，WD证明义务就是保证定义的时候不会出现类似于这样子的病态定义

Event-B建模（四）——Rodin平台使用及Event-B语言相关推荐

国产自主可控的MBSE建模与仿真平台SkyEye
转载: 2020年6月,哈工大.哈工程被美国商务部列入实体清单,禁用MATLAB事件频繁登上热搜,工业软件被称为「卡脖子」技术. 截止到2020年12月,中国已有超过300家企业和机构被列入美国&qu ...
Web3.0网关Deeper Network计划于本月末在四个平台上进行IDO
3月12日消息,旨在建立隐私和安全的 Web 3.0 网关 Deeper Network 计划于本月末在 Flybit.Ignition.Poolz 以及 DuckStarter 四个平台上进行为期四 ...
matlab火箭模型,基于Matlab/Simulink的新型火箭建模与仿真平台搭建
2018 年 11 月第 14 卷第 4 期系统仿真技术 System Simulation Technology Nov． ,2018 Vol． 14,No． 4 中图分类号: TP3 ...
mysql gtid深入_深入理解MySQL 5.7 GTID系列（四）:mysql.gtid_executedPREVIOUS GTID EVENT
之所以把MySQL.GTID_EXECUTED表的作用和PREVIOUS GTID EVENT的改变放到一起进行描述是因为它们后面文章探讨的基础.这部分使用到了我自己使用C语言写的原生BINLOG解析 ...
c语言实验四报告,湖北理工学院14本科C语言实验报告实验四数组
湖北理工学院14本科C语言实验报告实验四数组.doc 实验四数组实验课程名C语言程序设计专业班级 14电气工程2班学号 201440210237 姓名熊帆实验时间 5.12-5.26 实验 ...
php蜜欧斯,微信公共平台怎么连接数据库，开发语言是PHP
微信公共平台怎么连接数据库,开发语言是PHP0 我想开发一个微信公共平台,具体功能是输入关键词题号,自动回复这个题目的答案.题目数量在4000道左右.大约160W字本来我用的是网上DOWN的简易PHP ...
互金信用评分建模四步骤
一.数据描述数据采集具体而言,分别为交易事实表,用户信息表,商户分类信息表,以及银行卡信息表,它们之间的关系如图4所示.这四张表格分别通过不同的关键字连接,具体如下:a. 用户信息表可以通过用户手 ...
数据仓库专题（2）-Kimball维度建模四步骤
一.前言四步过程维度建模由Kimball提出,可以做为业务梳理.数据梳理后进行多维数据模型设计的指导流程,但是不能作为数据仓库系统建设的指导流程.本文就相关流程及核心问题进行解读. 二.数据仓库建设 ...
MATLAB数学建模(四)：机器学习
一.学习目标. (1)了解机器学习算法在数学建模中的应用. (2)掌握机器学习算法中的二分类.多分类.回归.聚类算法. 二.实例演练. 1.谈谈你对机器学习算法与数学建模的了解. 机器学习 ( Mac ...

Event-B建模（四）——Rodin平台使用及Event-B语言

目录

Rodin基本操作

Event-B表示法

证明义务

Event-B建模（四）——Rodin平台使用及Event-B语言相关推荐

最新文章

热门文章