Biomedical Engineering Reference
In-Depth Information
create animations at different stages of development of a simulated system. To do
so, a modeller may need to create an animation using the Macromedia Flash plug-in
for Brama. The use of this plug-in is established through a communication between
the animation and the simulation.
Brama is a tool allowing to animate Event-B models on the Rodin platform. It
allows animating and inspecting a model using Flash animations. Brama has two ob-
jectives: to allow the formal model's designer to ensure that his model is executed
in accordance with the system it is supposed to represent; to provide this model
with a graphic representation and animate this representation in accordance with
the state of the formal model. A modeller can represent the system manually within
Rodin [
46
] or represent the system with the Macromedia Flash tool that allows for
communication with the Brama animation engine through a communication server.
The graphic representation must be in Macromedia Flash format and requires the
use of a separate tool for its elaboration (Flash MX, for example). Once the Event-B
model is satisfactory (it has been fully proven, and its animation has demonstrated
that the model behaves like its related system), you can create a graphic representa-
tion of this system and animate it synchronously with the underlying Event-B Rodin
model. Brama does not create this animation. It is up to the modeller to create the
representation of the model depending on the part of the model he wants to display.
However, Brama provides the elements required to connect your Flash animation
and Event-B model [
48
].
5.5.6 Formal Modelling Language: Event-B
Event-B is a
proof-based
formal methods [
1
,
10
] for system-level modelling and
analysis of large reactive and distributed systems. In order to model a system, Event-
B represents in terms of
contexts
and
machines
. The set theory and first-order logic
are used to define contexts and machines of a given system. Contexts [
1
,
10
] contain
the static parts of a model. Each context may consist of carrier sets and constants
as well as axioms, which are used to describe the properties of those sets and con-
stants. Machines [
1
,
10
] contain the dynamic parts of an Event-B model. This part is
used to provide the behavioural properties of a model. A machine model is a state,
which is defined by means of variables, invariants, events and theorems. The use of
refinement represents systems at different levels of abstraction and the use of math-
ematical proof verifies consistency between refinement levels. Event-B is provided
with tool support in the form of an open and extensible Eclipse-based IDE called
Rodin [
46
] which is a platform for Event-B specification and verification.
5.6 Applications and Case Studies
We have applied our proposed approach of the real-time animator [
41
] in the de-
velopment of cardiac pacemaker [
40
] (see Chap.
9
). A cardiac pacemaker is a high
Search WWH ::
Custom Search