需求文档

现在有这么一座岛屿Island，有一座桥(Bridge)连通着大陆(Mainland)与这座小岛，而我们的系统主要功能是实现对桥上汽车的控制。

在这里我们的需求文档有两类需求，一些需求与控制器的功能有关，我们标记为FUN(Function的缩写)，另一些与环境有关，标记为ENV(Environment的缩写)。（和软件功能直接相关的需求标记FUN，而ENV标记是外部环境的需求，不由系统所控制）

系统的主要功能控制一座桥上的汽车，该桥连接着大陆和一座小岛

系统设备包括两个交通灯，交通灯的颜色为红色和绿色

交通灯控制着桥两端的入口，一个交通灯安装在大陆一端，另一个安装在小岛一端

假定汽车司机都服从交通灯的指挥，红灯行，绿灯停

系统装备了四个两状态传感器，状态有开和关闭

传感器用于检测汽车进入或者离开这座桥，两个传感器安装在桥上，另外两个分别安装在大陆和小岛上

桥上和小岛上的汽车数量有限制

桥是单行道，不能同时双向行驶

分析

我们先从一个非常简单的模型开始，其中只考虑了需求FUN-2，然后通过精化的方式，逐渐考虑更多的需求。

在第一个模型中，我们不准备考虑各种各样的设备（交通灯和传感器），也不准备考虑桥，现在先把桥和小岛看成一个组合体。

现在这个模型是极度抽象的，如下图所示：

并且这个模型有两个迁移动作ML_out和ML_in，分别表示汽车进入以及离开这个桥岛组合体，我们第一步工作就是形式化表示系统中的状态和事件。

前置准备

rodin版本3.4

插件安装
1)atelier B

2)SMT solvers

3)ProB

为了让我们的证明更加顺畅，我们要更改一下证明求解器，下载SMT插件，并且在这个位置把自动证明器改成SMT求解器，如果没有设置的话呢，就会出现某些证明证明不出来的情况

还有这个地方最好也更改一下，它的作用是某些使用单击更改的地方需要用双击更改，省得到时候一不小心点了一下就报错了

然后呢，rodin的小bug还是蛮多的，用的时候要耐心一点，多多F5刷新

新建工程

打开Rodin，新建一个工程

填写一个项目名称

状态的形式化

模型的状态由两个部分组成：静态部分和动态部分。

静态部分包含一些与常量相关的定义和公理，而动态部分包含着随着系统演化而可以被修改的部分。

静态部分也称为模型的上下文(context)，动态部分也称为机器(machine)

（其实machine和context最主要区别就是相关部分是否会发生变化，而不是下面框框里面的具体内容，例如machine和context都有定理(theorems)这部分，但machine就是和变化部分相关的定理，而context就是不变部分相关的定理）

模型状态的静态部分

第一个模型的上下文非常简单，只有一个常量d，它是一个自然数，表示出现在桥岛组合体上的最大汽车数。常量d有一条公理，它是自然数。

现在开始建一个上下文，上下文和机器都是模型的组件，在项目上右击，新建一个组件

选择下面的类型为context，组件名就随便取好了

先加入一个常量

在Rodin写东西可不是像写代码那么随意的哟，想要加入什么组件需要右键选择添加

把这个常量的名字改为d，接下来添加公理

∈和N符号在右下角的符号框可以找到，然后修改一下把这条公理的名字命名为axm0_1

模型状态的动态部分

动态部分只有一个变量n，代表某一个特定时刻，在桥岛组合体上的实际车辆数目，我们知道n同样是一个自然数，并且它肯定要小于等于d

再次右键，添加一个变量

然后添加n的约束，称为不变式（invariant），一个是n∈N，另一个是n小于等于

在上面添加一个see关系，表示这个机器观看（see）之前定义的机器ct。（机器和机器，上下文与上下文，上下文与机器之间有多种关系，这里先不讨论）

最后不得不先提一个动作的概念，在EVENTS栏目下的INITIALISATION事件中右键添加一个动作（Action），然后给n赋值0，因为Rodin所有变量都需要赋予初始值，不然会警告。

事件的形式化

OK，完成了状态的形式化，接下来就是事件的形式化工作

事件相当于因为系统发生了某种变化而导致系统的状态发生迁移，这个系统的事件有两个，分别是汽车进入或者离开桥岛组合体，这两个分别对应ML_out和ML_in，当汽车进入桥岛组合体时，会使得n加1，而汽车离开桥岛组合体时，会导致n减1

当然啦，在n加1减1的时候还要考虑n是否在边界值上，只有当n<d的时候才能执行n=n+1，而当n的值大于0的时候才能执行n=n-1，不然就明显错误了，这种使得一个事件能够执行的必要条件，称为卫(guard)

下面在Rodin中对事件部分进行构建

右键添加两个Event，分别命名为ML_out和ML_in

右键添加guard作为条件，加入action作为动作

证明义务

我们看到rodin的左边explorer里，点开mac1的Proof Obligations

这里面的就是证明义务，由rodin自动帮助我们生成，旁边的绿色的代表已证明，如果是红色的说明证明出现了问题，无法完成自动证明，这时候可以双击点进去看看到底是出了啥问题

证明义务的命名是一个组合名字，例如ML_out/inv1/INV，说明这是一个有关不变式保持的证明义务，因为ML_out在执行的时候会改变变量n的值，在改变过程中可能就会违反不变式，所以需要对此进行相应的证明。

因为这里的建模相对完备，所以都证明好啦

无死锁证明

我们的系统中有了两个卫，但有可能发生一种情况，即这两个卫都为假，模型就发生了死锁，当然啦，根据系统的不同，有时候也是可以发生死锁的，但显然我们的系统应该一直运行下去，所以在需求文档中，我们加入这么一行：

一旦系统开始执行，这个系统就应该永远工作下去

我们在不变式这里加上一条thm1， n<d∨0<nn<d\text{ }\vee\text{ }0<nn<d ∨ 0<n，然后点击not theorem，把它改成theorem，它表示不能出现同时不满足两个卫的情况

看到左边explorer这里多了一条证明义务，不过它标红了，是不是漏了什么呢？

我们双击进去看看，点击rodin右上角的proving视图

我们想到，当n和d都为0的时候就不满足无死锁性质了，但d明显不应该是0，所以是我们之前漏掉了一个重要的条件，d应该为正数

回到ct，加上d>0这个公理

重新保存，我们发现证明义务全都证明完成了

至此，我们的初始模型构建完毕

解决出现的问题

好~如果你照着敲并且出现了问题，那基本上就是你的问题，可以遵循以下思路尝试解决问题
1、rodin版本是否正确，我这里是3.4
2、插件都装上了嘛？特别是SMT这个还要设置以下
3、真的敲的一样嘛？看看符号什么有没有弄错
4、看看后面的not theorem，theorem,extend，ordinary，convergent之类的有没有设置完成，或者有没有误点
5、保存了吗？没有保存的话肯定证明不出来
6、在报错的证明义务下右键，点击retry auto provers，很多时候就好了

总之就是要多尝试，多总结~

该篇文章的后续Event-B建模（六）——控制桥上汽车，精化

Event-B建模（三）——控制桥上汽车，初始模型相关推荐

Event-B建模（六）——控制桥上汽车，精化
目录第一次精化状态的精化事件的精化第二次精化状态的精化事件的精化第三次精化状态的精化事件的精化这篇的上一篇在这个地方Event-B建模(三)--控制桥上汽车,初始模型,环境配置和小 ...
线性系统大作业——2.二阶倒立摆建模与控制系统设计（上）
文章目录 0.简介 1.建立数学模型 1.1.牛顿运动定律分析欧拉-拉格朗日方程分析 2.Simulink仿真 3.使用SimMechancis仿真 4.在平衡点附近模型线性化 5.系统能控性.能观 ...
MATLAB优化转向器,汽车电动转向器动力学建模与控制仿真研究(MATLAB仿真)
汽车电动转向器动力学建模与控制仿真研究(MATLAB仿真)(任务书,开题报告,外文翻译,计划进度表,毕业论文12000字,相关框图和参数) 摘要汽车电动转向器是一种新型的汽车转向助力系统. 文章 ...
超牛！用WIFI控制的摇控汽车
(今天在PCClub上看到一牛人的帖子,拿来和大家分享下.) 超牛!用WIFI控制的摇控汽车一.前言 Wifi机器人(Wifi Robot):其实是一辆能通过互联网,或500米以外的笔记本无线设施来 ...
《机器人与数字人：基于MATLAB的建模与控制》——2.3节指数映射和k过程
本节书摘来自华章社区<机器人与数字人:基于MATLAB的建模与控制>一书中的第2章,第2.3节指数映射和k过程,作者［美］顾友谅(Edward Y.L.Gu),更多章节内容可以访问云栖社区 ...
19个神经元控制自动驾驶汽车，MIT等虫脑启发新研究登Nature子刊
本文经机器之心(almosthuman2014)授权转载,禁止二次转载. 选自Medium 作者:Louis Bouchard 机器之心编译编辑:魔王.泽南这种新型智能系统模仿线虫的神经系统来高效 ...
当AI邂逅生命健康，华为云为他们搭建三座桥
2020年11月,AlphaFold2在蛋白质结构预测大赛CASP 14中大显身手,将AI+生命健康的全球热度推到了新的高峰.事实上,早在此之前AI赋能大健康.医疗.制药等领域就是广受关注的话题.尤其 ...
两轮差速移动机器人运动分析、建模和控制
两轮差速运动分析.建模和控制 1 运动学分析建模 1.1 三种运动状态分析 1.2 函数模型 1.3 仿真验证 1.3.1 直线验证 1.3.2 曲线验证 1.3.3 旋转验证 2 运动控制 2.1 ...
《机器人与数字人：基于MATLAB的建模与控制》——2.2节李群和李代数
本节书摘来自华章社区<机器人与数字人:基于MATLAB的建模与控制>一书中的第2章,第2.2节李群和李代数,作者［美］顾友谅(Edward Y.L.Gu),更多章节内容可以访问云栖社区&q ...

Event-B建模（三）——控制桥上汽车，初始模型

目录