Naslov
Model Checking of Concurrent System with SDL-- Specification

Autori
Blašković, Bruno ; Dembitz, Šandor ; Knežević, Petar ;

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
10th Mediterranean Electrotechnical Conference, Melecon 2000, Vol. l / Economides, Costas. Patticichis, Constantinos. Maliotis, Gregory - Nikozija : Violaris Press Ltd, Nicosia, Cyprus, 2000, 77-80

Skup
10th Mediterranean Electrotechnical Conference, Melecon 2000

Mjesto i datum
Nikozija, Cipar, 29.05.2000. - 31.05.2000

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
model checking; verification of specification; SDL; SPIN; concurrency; protocol synthesis

Sažetak
It is well known that the best results regarding concurrent system design are obtained when design errors are find in earlier possible phase. For that purpose system specification is verified through model shecking. We try to hidden as much as possible model checking formalism from designers viewpoint. First, a system is modeled as set of processes described formaly as extended finite state machine within SDL-- language. Suvh description is translated into model checker SPIN where desired properties are verified. Special attention is given to the possibility of modelling 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.

Izvorni jezik
Engleski

Znanstvena područja
Elektrotehnika

POVEZANOST RADA