Pretražite po imenu i prezimenu autora, mentora, urednika, prevoditelja

Napredna pretraga

Pregled bibliografske jedinice broj: 64540

Model Checking of Concurrent System with SDL-- Specification


Blašković, Bruno; Dembitz, Šandor; Knežević, Petar;
Model Checking of Concurrent System with SDL-- Specification // 10th Mediterranean Electrotechnical Conference, Melecon 2000, Vol. l / Economides, Costas. Patticichis, Constantinos. Maliotis, Gregory (ur.).
Nicosia: Violaris Press Ltd, Nicosia, Cyprus, 2000. str. 77-80 (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)


CROSBI ID: 64540 Za ispravke kontaktirajte CROSBI podršku putem web obrasca

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 - Nicosia : Violaris Press Ltd, Nicosia, Cyprus, 2000, 77-80

Skup
10th Mediterranean Electrotechnical Conference, Melecon 2000

Mjesto i datum
Nikozija, Cipar, 29-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


Projekti:
036021

Ustanove:
Fakultet elektrotehnike i računarstva, Zagreb

Profili:

Avatar Url Šandor Dembitz (autor)

Avatar Url Petar Knežević (autor)

Avatar Url Bruno Blašković (autor)


Citiraj ovu publikaciju:

Blašković, Bruno; Dembitz, Šandor; Knežević, Petar;
Model Checking of Concurrent System with SDL-- Specification // 10th Mediterranean Electrotechnical Conference, Melecon 2000, Vol. l / Economides, Costas. Patticichis, Constantinos. Maliotis, Gregory (ur.).
Nicosia: Violaris Press Ltd, Nicosia, Cyprus, 2000. str. 77-80 (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)
Blašković, B., Dembitz, Š., Knežević, P. & (2000) Model Checking of Concurrent System with SDL-- Specification. U: Economides, Costas. Patticichis, Constantinos. Maliotis, Gregory (ur.)10th Mediterranean Electrotechnical Conference, Melecon 2000, Vol. l.
@article{article, author = {Bla\v{s}kovi\'{c}, Bruno and Dembitz, \v{S}andor and Kne\v{z}evi\'{c}, Petar}, year = {2000}, pages = {77-80}, keywords = {model checking, verification of specification, SDL, SPIN, concurrency, protocol synthesis}, title = {Model Checking of Concurrent System with SDL-- Specification}, keyword = {model checking, verification of specification, SDL, SPIN, concurrency, protocol synthesis}, publisher = {Violaris Press Ltd, Nicosia, Cyprus}, publisherplace = {Nikozija, Cipar} }
@article{article, author = {Bla\v{s}kovi\'{c}, Bruno and Dembitz, \v{S}andor and Kne\v{z}evi\'{c}, Petar}, year = {2000}, pages = {77-80}, keywords = {model checking, verification of specification, SDL, SPIN, concurrency, protocol synthesis}, title = {Model Checking of Concurrent System with SDL-- Specification}, keyword = {model checking, verification of specification, SDL, SPIN, concurrency, protocol synthesis}, publisher = {Violaris Press Ltd, Nicosia, Cyprus}, publisherplace = {Nikozija, Cipar} }




Contrast
Increase Font
Decrease Font
Dyslexic Font