Model checking of concurrent system with SDL/sup --/ specification (CROSBI ID 717465)
Prilog sa skupa u zborniku | sažetak izlaganja sa skupa | međunarodna recenzija
Podaci o odgovornosti
Blaskovic, B. ; Dembitz, S. ; Knezevic, P.
engleski
Model checking of concurrent system with SDL/sup --/ specification
It is well known that the best results regarding concurrent system design are obtained when design errors are found in the earliest possible phase. For that purpose system specification is verified through model checking. We try to hide, as much as possible, the model checking formalism from the designers viewpoint. First, a system is modeled as a set of processes described formally as an extended finite state machine within the SDL/sup --/ language. Such a description is translated into the model checker, SPIN, where the 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 an approach the designer can have the, SDL/sup --/ specification verified against the desired properties.
specification languages, formal specification, formal verification, multiprocessing systems, finite state machines, reachability analysis
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
77-80.
2000.
objavljeno
10.1109/melcon.2000.880372
Podaci o matičnoj publikaciji
Proceedings of 10th MELECON
Economides, C.
Lahti: Institute of Electrical and Electronics Engineers (IEEE)
Podaci o skupu
MELECON - Mediterranean Electrotechnical Conference
predavanje
29.05.2000-31.05.2000
Limassol, Cipar