Naslov
Model checking of concurrent system with SDL/sup --/ specification

Autori
Blaskovic, B. ; Dembitz, S. ; Knezevic, P.

Vrsta, podvrsta i kategorija rada
Sažeci sa skupova, sažetak, znanstveni

Izvornik
Proceedings of 10th MELECON / Economides, C. - Lahti : Institute of Electrical and Electronics Engineers (IEEE), 2000, 77-80

Skup
MELECON - Mediterranean Electrotechnical Conference

Mjesto i datum
Limassol, Cipar, 29.05.2000. - 31.05.2000

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
model checking , design errors , reachability , concurrent system design , system specification , extended finite state machine , SDL/sup --/ language , model checker , SPIN transitions modeling, specification verification , formal description techniques
(specification languages, formal specification, formal verification, multiprocessing systems, finite state machines, reachability analysis)

Sažetak
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.

Izvorni jezik
Engleski

Znanstvena područja
Elektrotehnika, Računarstvo

POVEZANOST RADA