Model checking of concurrent system with SDL-- specification

It is well known that the best results regarding concurrent system design are obtained when design errors are And in the earliest possible phase. For that purpose system specification is verified through model checking. We try to hidden as much as possible model checking formalism from designers viewpoint. First, a system is modeled as set of processes described formally as extended finite state machine within SDL-- language. Such description is translated into model checker SPIN where desired properties are verified. Special attention is given to the possibility of modeling various types of transitions and to a definition of the tool where model checking is performed. With such approach designer can have SDL-- specification verified against desired properties.