ISSN: 0970-938X (Print) | 0976-1683 (Electronic)

An International Journal of Medical Sciences

Research Article - Biomedical Research (2017) Artificial Intelligent Techniques for Bio Medical Signal Processing: Edition-I

In this paper, we discuss about the specification of timed state transition systems that communicate by binary and rendezvous interactions. The observed approach unfolds the state machines according to synchronization and timing requirements. The unfolded state transition diagrams has been used to approximate a global time and to verify the safety, liveness and fairness properties of the system. A Master, Worker and Assembler of laser speckle image processing system in biomedical engineering are used as running example to illustrate the approach and properties.

Timed CFSMs, Unfolded CFSMs, State explosion, Interleaving semantics, Partial-ordered semantics.

With the increasing use of computers in medical imaging , there is a pressing need for designing more reliable systems. As a result, developing formal methods for the design and analysis of concurrent systems has become an active area in computer science and biomedical engineering research. Traditional testing method such as simulation is inadequate for developing bug-free complex and concurrent systems. One approach to ensure correctness is to employ automatic verification method. A verification formalism consists of [1]:

• A formal semantics to assign mathematical meaning to system components and its correctness criteria;

• A language for describing the constructs for combining the components;

• A specification language for expressing the correctness requirements;

• A verification algorithm to ensure that correctness criteria are fulfilled in every possible execution of the system.

Real-time system performances are used in medical image processing system. Failures in such systems can be very expensive and even life-threatening and consequently there is a great demand for formal methods that should be applied to real-time systems. Different formalisms have been proposed to reason reactive systems. These include process algebra, temporal logics, Petri Nets, automata theoretic techniques and partial-order models [1]. In the traditional approach for verification of concurrent programs, the correctness of the program is expressed by a formula in first-order temporal logic. The verification reduces to proving a theorem in a deductive system. Model-checking provides a different approach to check the properties of finite state systems [1-8]. In this approach, the global state transition graph is viewed as a finite Kripke structure. The specification of the system is given as a formula of a propositional temporal logic. The modelchecking algorithm decides whether a system meets the specification in all possible executions or not.

The model-checking approach used for program verification is probably the most exciting advance in the theory of program correctness in recent years. The main difficulty in using modelchecking approach is the state-space explosion problem. The size of the global state-transition graph grows exponentially with the number of components in the system. There are many ways to avoid this problem [1-8]. In this work, the partialordered unfoldings of CFSMs (Communicating finite state machine) are constructed to avoid the state-explosion in constructing a single total-ordered global-state transition graph (also known as product machine).the above method is achieved by simulating each local CFSMs in the presence of non-local CFSMs and performing the synchronizations. Section 2 defines the preliminaries of the CFSMs and their unfolding using a real time laser speckle image processing in biomedical image processing system.

Here it is assumed that specification of n CFSMs are nonterminating [2]. The CFSMs interact by synchronous messagepassing via a binary rendezvous based on the seminal work of CSPs (Communicating Sequential Processes) [9,10]. The simultaneous n-ary (multiparty) interaction is split into a sequence of two party rendezvous interactions using a queue.

In a set of n communicating and non-terminating FSMs, each CFSM is defined as a 7-tuple:

Definition 1. A CFSM *Fi* = (s_{0fi}, *S*_{fi}, *A*_{fi}, *C*_{fi}, *R*_{tfi}, *Rsync*_{fi}, *Rsync*_{0fi}) where,

S_{fi} is the finite set of states of CFSM F_{i}, s_{0fi} ϵ S_{fi} being the
initial state.

A_{fi} is the finite set of asynchronous and synchronous actions of
F_{i}.

C_{fi} is the set of clock variables of F_{i}

R_{tfi} is a transition relation such that:

In i-transition (*s*_{fi}, *a*_{fi}, *g*_{fi}, *u*_{fi}, *s*’_{fi}) ϵ *R*^{tfi}, s_{fi} is called the input
state and s’_{fi} the output state. a_{fi} is the action label, g_{fi} is the
guard which is the enabling condition of the transition based on
clock variables C_{fi}, (default being True), u_{fi} is the update
statement again based on clock variables (default being Null
statement) executed upon the transition. If the enabling
condition g_{fi} is True, the transition is considered instantaneous
and if g_{fi} is of the form (x_{i} ≥ t_{i}), x_{i} ϵ C_{fi}, the transition takes at
least ti time units to enter the next state s’_{fi} from s_{fi}. In the case
of a synchronous transition, the send action is denoted as A_{fi}!
and the corresponding receive action as A_{fi}? in the partner
CFSM F_{j}, j ≠ i.

• is a binary relation which relates the output states of synchronous transitions.

• relates the set of pairs of initial states: All the initial states are assumed to be in pairwise synchronous with each other to begin with.

• **Figure 1** shows an example of worker, master and
assembler CFSMs [11]. When there is more than one
worker in a simultaneous approach, the master serves one
worker at a time, making the other worker wait in a queue.

*The unfolding of CFSMs*

**Definition 2:** The unfolded CFSM *M _{i}* = (s

**Figure 2** shows the unfolded CFSMs of the worker t_{i}, master
and the assembler. The master is considered as the anchoring
agent as it synchronizes both the worker agent and assembler
agent/process. T_{ti}, T_{m} and T_{a} are the variables monitoring the
local times of the worker, master and assembler agents,
respectively. The local time of each agent at every state-entry,
is initialized to zero. Thus T_{ti}=0, T_{m}=0 and T_{a}=0, respectively
at states Sw_{i0}, Sm_{0} and Sa_{0}. At every local output state entry,
for instantaneous transition, the time remains the same as that
of the input state entry. For non-instantaneous transition the
local time is updated corresponding to the duration of the
transition as dictated by its guard g_{fi}(C_{fi}). For instance, if the
synchronous transition pair *appri*! and *appr*? respectively from
states Sw_{10} and Sm_{0} are instantaneous then T_{t1}=0 and T_{m}=0 at
the respective output states St_{11} and Sm_{1}. At every rendezvous/
synchronization point, the state entry times of both
synchronous output states are normalized to maximum of the
corresponding local times. After the transition pair *lower*! and *lower*? from states Sm_{1} and Sa_{0} respectively, the local clock
constraint of guard z<1 dictates Tm=1 at Sm2. Even though
there is no such constraint for the assembler agent’s *lower*? action, the local time T_{a} at Sa_{1} is normalized to the maximum
one, viz., T_{m}=1, same as master. Thus the local time is
propagated at synchronization point and becomes logically a
semi-global time. Hence the anchoring agent master,
propagates the worker’s local time to the assembler agent and
vice versa. Rest of the local time updates are shown in **Figure
2**.

*Well-founded, partially-ordered causality generation*

When the CFSM graphs are unwinded in their mutual global
environments into trees by simulating each of the former in
their respective non-local environments, it tends to generate a
global causality which is a partial-order. The global, temporal
causality order is composed using the binary relations Rsync_{i} and R_{i}, i ϵ {1..n} as follows [2]:

≤ ::= (R_{i} U Rsync_{i})*

The binary successor relation R_{i} is R_{ti} with input and output
states related. The binary relation represents the partially
ordered, and well-founded causality relation among the states
of CFSMs in the unfolding based on their points of entry in
time. The Rsynci relations capture the equality in time of the
synchronous output states.

The unfolded timing diagram is shown in **Figure 2**. Each local
state of the unfolding CFSM stores the local time, which is
updated according to local clock constraint after asynchronous
local transitions. After every synchronous transition, the local
time is updated to the maximum of the two synchronizing
FSMs. Thus, an approximate global time is synthesized by
propagating the maximum advanced local times of the
communicating FSMs.

Initially the worker-i is in state Sw_{i0} and the master is in state
Sm_{0} and the assembler in Sa_{0}. The approach of the first worker
is captured by the pair of transitions *approachi*! by the sending
worker and *approach*? by the receiving master from the
corresponding local states Sw_{i0} and Sm_{0} respectively. If there
is more than one worker approaching simultaneously, one of
them is selected from the head of the list/queue L and the
others are made to wait in the queue. T_{ti}, the local time of
worker ti is set to 0, T_{ti}=0, and similarly the local time of
master is set to 0, T_{m}=0 after the instantaneous transition pair *approach!/approach?* reaching states Sw_{i1} and Sm_{1} respectively. Next, the master sends lower! signal to the
assembler which receives it by its corresponding *lower*?
transition within a maximum of 1 minute. Therefore at the end
of *lower!/lower?* pair of synchronous transitions, the local times of master and assembler are, T_{m}=1 and T_{a}=1 at states
Sm_{2} and Sa_{1} respectively. Next, the worker ti makes a local
asynchronous transition in x>2 minutes. If T_{ti}=3, at state Sw_{i2} following the local clock constrint of x>2. Then, worker t_{i} makes another local transition out which is instantaneous,
reaching Sw_{i3}. The local time of worker t_{i} remains T_{ti}=3 in
state Sw_{i3} and so on. The remaining transitions and local times
are shown in **Figure 2**. Because of the fact that the master is
synchronizing with assembler and the worker t_{i} independently
and at each synchronization point the local times are updated to
the maximum, deducing the logical global time of the observer,
observing all the three parties/processes [12-14].

*The elimination of state-explosion due to nondeterministic
interleaving in unfolded CFSMs*

Consider a conventional product machine composed of two
component CFSMs. Assume a state vector (s_{1}, s_{2}) of the
product machine with s1 representing the state of CFSM_{1} and
s_{2} representing that of CFSM_{2}. Consider two local/
asynchronous state transitions (s_{1}, a_{1}, s’_{1}) and (s_{2}, a_{2}, s’_{2}) of
CFSM_{1} and CFSM_{2}, respectively. In the traditional
construction of the product machine, these two transitions are
modeled by choosing either one of the two transitions to
happen first followed by the other in sequence. This would
lead to the following product machine state transitions as
shown in **Figure 3**. Consisting of 2^{2}=4 transitions representing the 2 independent local/asynchronous transitions of CFSM_{1} and CFSM_{2}. To extend this representation of non-deterministic
interleaving to n different local/asynchronous transitions of n
respective CFSMs, CFSM_{1}, CFSM_{2} … CFSM_{n}, it would need
2^{n} transitions to represent n independent asynchronous
transitions of the n CFSMs in the case of product machine. On
the other hand, in the case of the unfolded CFSMS, the n local/
asynchronous transitions of the n CFSMs would be modeled by
exactly n transitions. This is the main advantage of the
partially-ordered CFSM unfoldings where the exponential
explosion of states due to non-deterministic interleaving is
avoided due to maintains of the locality of each CFSM.

A specification of timed CFSMs with a worker, assembler, master of laser speckle image processing system in biomedical engineering , is illustrated to specify and model-check the safety, liveness and fairness properties of a timed communicating agent. With the help of temporal logic verification model checking is to be done in author’s future work. The state-explosion problem of model-checking is eliminated by avoiding the product machine construction of interleaving semantics, using the unfolded CFSMs of partialorder semantics.

- Alur R. Techniques for Automatic verification of Real-time systems, Ph.D. Thesis. Stanford Yniversity, 1991.
- Narayanan VK. A state-oriented, Partial-order model and Logic for Distributed Systems Verification, Ph.D. Thesis, Concordia University, Montreal, 1997.
- Clarke EM. Progress on the state-explosion problem in model-checking. Informatics 2001.
- McMillan KL. Symbolic Model Checking: An approach to the state explosion problem, Ph.D. Thesis, 1992, CMU-CS-92-131.
- Clarke EM, Emerson EA. Synthesis of synchronization skeletons for branching time temporal logic. Logic of Programs: Workshop, LNCS, 1981.
- Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite-state concurrent system using temporal logic. In Proceedings of the Tenth Annual ACM Symposium on Principles of Programming Languages (POPL), 1983.
- Clarke EM, Grumberg O, Peled D. Model Checking. MIT Publishers, 1999.
- Clarke EM, Schlingloff H. Model checking. Robinson J and VoronkovA , Ed, Handbook of Automated Reasoning. Elsevier, 2000.
- Park J. A Theorem Prover for Boolean BI. ACM International conference on Principles of Programming Language POPL, 2013.
- Hoare CAR. Communicating Sequential Processes. Prentice Hall 1984.
- Yiqun C. Parallel and Distributed computing Techniques in Biomedical Engineering, Ph.D. Thesis, 2005.
- Dakshinamurthy S, Narayanan V. A fully-distributed checkpointing-protocol for fault-tolerance in real-time distributed systems, in National IETE Conference, 2012.
- Dakshinamurthy S, Narayanan V. A parallel algorithm for model-transformation of interactive state machine specification. Int J Wisdom Based Comput 2012.
- Dakshinamurthy S, Narayanan V. A Model-checking Algorithm for Formal verification of Peer-to-peer Fault-Tolerant Networks, ICIWE 2013.
- Yi W, Pettersson P, Daniels M. Automatic verification of real-time communicating systems by constraint-solving. In Formal Description Techniques VII. Springer US, 1995.