【1】事件上，精化模型的Guard要能推出抽象模型的Guard
【2】抽象模型上新增加的事件，相当于继承自skip
Guard: true
Actions: a:=a,b:=b,c:=c,...
【3】抽象模型上新增加的事件不能是发散(divergence)，即不能有活锁(没有对外反馈，内部一直执行)。这个的证明是添加一个变式variant，一方面证明它是自然数NAT，一方面是证明事件做完variant减少，合之就说明事件收敛。variant不在原来的模型里，当要证明新事件收敛时要额外添加这个参数。
在Rodin平台上，把新增加的event的ordinary改成convergent，就是要告诉它这个event要被证明是收敛的(把证明意图告诉系统)，改完要刷新一下。这时候保存会报warning，提示没有variant，接着就在新模型里右键增加variant。只要能找到这样一个变式，使得每个新事件的运行都使这个变式减少，就能说明所有新事件都是收敛的了，这里要靠自己去想去构造它。
【4】无死锁的证明义务，只要抽象模型有能运行的事件，那么具体模型也要有能运行的事件。这是一个可选的证明义务，不是必须的，因为即使发生死锁也和抽象模型不冲突，因为不做事情就不会出错。
Event-B一些基本内容
猜你喜欢
转载自www.cnblogs.com/LauZyHou/p/12691746.html
今日推荐
周排行