On deriving the parallel composition of extended finite state machines

In this paper we consider a problem of communicating components of telecommunication systems. The components interact not only with each other but also with an environment. The interaction is in a dialog mode and the so-called “slow environment” condition takes place. As usual, each component of the system is a software. An Extended Finite State Machine (EFSM) allows to describe the software. In order to verify and test the communicating components we need a formal description of the system. It is well known how to get such description for the case when each component is described as a classical Finite State Machine (FSM). However, it is not always possible to derive an equivalent FSM for the appropriate EFSM. The first reason is that domains of input / output parameters and context variables can be infinite. The second one is that even domains are finite we can face to so-called state explosion problem. So in this paper we discuss approaches how to describe the composition of EFSMs in case when one of components is embedded. There are two approaches to derive the composition of FSMs. One of them is based on transformation of each FSM into corresponding automaton. These automata are composed and then the composition is transformed into an FSM. Unfortunately, we can't use this approach because we don't know how to transform the EFSM into automaton. The second approach is based on derivation of reachability tree. In this case, the composition at a stable state accepts an external input, moves through intermediate states (an internal dialog between components), reaches new stable state and produces an external output. The composition has only stable states and transitions between these states are marked by external inputs and outputs. And we adopted this approach for the case of EFSM's composition. We have formulated two conditions when this approach is valid for EFSMs. If for each internal input the Context produces an external output and predicates of Context don't depend on output parameters of Embedded component, then it's possible to construct a composition of EFSMs without derivation equivalent FSMs. The second condition is that the approach is valid if there is not more than one transition with predicate in internal dialog between components.

Keywords

Authors

References