Formal Logic Based Heart-Model - Using Event-B for Critical Device Software Systems - page 151

SA Block
This block occurs within the SA node (A) and is described as an SA nodal block
or sick sinus syndrome. The SA node fails to originate an impulse, and the heart
misses one or two beats at regular or irregular intervals (see Fig. 8.7 (a)).
AV Block
For an AV block, the sinus rhythm is normal, but there is a conduction defect be-
tween the atria and the ventricles. The main cause of this block may be in the AV
node (B) or the Bundle of His (D), or both (see Fig. 8.7 (b)).
Infra-Hisian Block
Blocks that occur below the AV node (B) are known as Infra-Hisian blocks (see
Fig. 8.7 (c)). This block describes block of the distal conduction system and it in-
cludes Type 2 second degree heart block.
Left Bundle Branch Block
In the normal heart, activation of both ventricles takes place simultaneously. A left
bundle branch block occurs when conduction into the left branch of the Bundle of
His is interrupted. Blocks that occur within the fascicles of the left bundle branch
are known as hemiblocks (see Fig. 8.7 (d)).
Right Bundle Branch Block
A right bundle branch block occurs when conduction into the right branch of the
Bundle of His is interrupted (see Fig. 8.7 (e)).
8.4.2 Cellular Automata Model
A set of spatially distributed cells form a CA model, which contains a uniform
connection pattern among neighbouring cells and local computation laws. CA were
originally proposed by Ulam and von Neumann [ 40 ] in the 1940s to provide a formal
framework for investigating the behaviour of complex, spatially distributed systems.
CA are discrete dynamic systems corresponding to space and time. CA modelling
involves uniform properties for state transitions and interconnection patterns. The
model components are specified by a single property caused by the same patterns