Event-B入门教程：系统建模与设计

4星 · 超过85%的资源需积分: 34 127 浏览量更新于2024-07-30 2 收藏 1.44MB PDF 举报

"《System Modelling & Design Using Event-B》是由Ken Robinson编写的关于Event-B技术的入门书籍，旨在介绍该建模语言的详细语法和使用方法。" Event-B是一种形式化建模方法，用于系统建模和设计，特别是在软件工程领域。它强调的不是编程，而是软件工程中的系统分析和设计，利用数学逻辑而非魔法般的技巧来确保系统的正确性。该技术起源于20世纪90年代，是基于Rodin平台的一个强大的工具集。在Event-B中，核心概念包括上下文(Context)、机器(Machines)、状态(State)、事件(Events)、证明(Proof)和精炼(Refinement)。上下文定义了系统的静态属性，机器描述了系统的动态行为。事件表示系统中可能发生的改变，而证明则是验证系统行为符合预期的关键步骤。机器的概念在Event-B中至关重要。例如，书中提到的“Coffee Club”示例，展示了如何构建一个简单的机器模型。证明义务(Proof Obligations, POs)是验证机器正确性的必要条件，通过sequent representation进行表达。理解并解决这些证明义务是使用Event-B的关键。精炼是Event-B中的一个重要概念，它允许从抽象模型逐步细化到更具体的实现。精炼规则指导了这个过程，如书中展示的“Coffee Club”的精炼案例，以及如何处理上下文成员和会员资格的精炼。精炼过程中会引入新的证明义务，需要识别和解决这些义务以确保精炼的正确性。动画(Animation)是Event-B的另一个关键特性，用于模拟和验证模型的行为。动画约束确保模型的动态行为符合预设的限制。书中还通过平方根计算的例子展示了如何进行精炼。这个例子说明了如何定义和建模问题，然后通过精炼步骤推进解决方案，包括参数的使用和收敛与变种的概念，这些都确保了求解过程的逐步完善和正确性。《System Modelling & Design Using Event-B》是一本深入介绍Event-B技术的教材，适合想要学习和掌握这一形式化建模方法的初学者。通过书中丰富的实例和解释，读者可以了解到Event-B如何用于构建和验证复杂系统的正确性。

10 CHAPTER 3. CONTEXTS, MACHINES, STATE, EVENTS, PROOF AND REFINEMENT

Consistently with the above, a single event may be reﬁned by multiple events, or conversely, multiple

events may be reﬁned a single event.

New events As well as reﬁnements of the events of the machine being reﬁned, the reﬁned machine

may introduce new events, but the new events must not change the state of any included from the

reﬁned machine. This is a restriction that recognises that a machine state can be modiﬁed only by the

events of that machine, or their reﬁnements.

Reﬁnement of the CoﬀeeClub

At the moment the CoﬀeeClub simply describes a piggybank that models an amount (of money), and

events that describe adding to —FeedBank— or taking from —RobBank— the amount modelled by

piggybank. We will now model behaviour that describes club-like behaviour for members who want to

be able to purchase cups of coﬀee. We will introduce variables members, accounts and coﬀeeprice and

events that correspond to

a new member joining the club: each member of the club is represented by a unique identiﬁer that

is arbitrarily chosen from an abstract set MEMBER;

a member adding money to their account: each member has an account, to which they can add

“money”;

a member buying a cup of coﬀee: there will be a variable, coﬀeeprice, representing the cost of a

cup of coﬀee, and each member can buy a cup of coﬀee provided they have enough money in their

account.

The value of all money added to accounts is added to piggybank.

Contexts Contexts are used in Event-B to deﬁne constant values such as abstract sets, relations, func-

tions; properties of those constants, called axioms and theorems expressing properties of the constants

that can be deduced from the axioms. The abstract sets are sometimes called carrier sets.

Concepts

axiom an axiom is a property that is asserted; it cannot be proved

theorem a theorem is a property that is implied by axioms or invariants; it must be proved

For this reﬁnement we need to deﬁne an abstract set MEMBER, which we will use as the source of

unique identiﬁers for members. The set is not given a speciﬁc size (cardinality), but it is declared to

be ﬁnite, meaning that it does have a size (cardinality) that is a natural number. Sets are potentially

inﬁnite, unless declared otherwise. Note that in Event-B inﬁnity is not a natural number.

Context MembersContext

context MembersContext

sets

MEMBER

axioms

axm1:

ﬁnite(MEMBER)

end

剩余141页未读，继续阅读

x314951220

粉丝: 0
资源: 10

Event-B入门教程：系统建模与设计

Rodin用户指南：入门与系统开发详解

OSGI实战：从入门到精通-Equinox框架解析

OSGI经典入门与实战教程

event-B入门基础手册

Node.js快速学习入门

零基础入门学习Python pygame文档

pygame入门

委托，最有价值的委托学习资料，委托入门，委托大全

1. Vue-WebGIS项目入门详解：理解SuperMap iClient JavaScript

cocos2d-lua热更新入门指南

最新资源