Distributed Behavior Protocol Checker

Growth of the computability power in the last years enabled practical use of model checking of software systems. However the state space explosion is still a burning problem that limits usage of this technique to the relatively small tasks. One of the approaches that significantly decrease state space of the task is Behavior Protocol [1]. Behavior protocol is regular language that describes behavior of software component so that component implementation details are hidden during checking of whole application - what is reduced to the checking whether behavior protocols of used components are compliant. However even checking of behavior protocols compliance faces the exponential growth of number of states. Distributed state space traversing together with 'on the fly' state space generation [2] can be used to improve both time and space requirements