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

Napredna pretraga

Pregled bibliografske jedinice broj: 1192744

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


Blaskovic, B.; Dembitz, S.; Knezevic, P.
Model checking of concurrent system with SDL/sup --/ specification // Proceedings of 10th MELECON / Economides, C. (ur.).
Cyprus: IEEE, 2000. str. 77-80 doi:10.1109/melcon.2000.880372 (predavanje, međunarodna recenzija, sažetak, znanstveni)


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

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. - Cyprus : IEEE, 2000, 77-80

Skup
MELECON - Mediterranean Electrotechnical Conference

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


Ustanove:
Fakultet elektrotehnike i računarstva, Zagreb

Profili:

Avatar Url Petar Knežević (autor)

Avatar Url Šandor Dembitz (autor)

Avatar Url Bruno Blašković (autor)

Poveznice na cjeloviti tekst rada:

doi ieeexplore.ieee.org

Citiraj ovu publikaciju:

Blaskovic, B.; Dembitz, S.; Knezevic, P.
Model checking of concurrent system with SDL/sup --/ specification // Proceedings of 10th MELECON / Economides, C. (ur.).
Cyprus: IEEE, 2000. str. 77-80 doi:10.1109/melcon.2000.880372 (predavanje, međunarodna recenzija, sažetak, znanstveni)
Blaskovic, B., Dembitz, S. & Knezevic, P. (2000) Model checking of concurrent system with SDL/sup --/ specification. U: Economides, C. (ur.)Proceedings of 10th MELECON doi:10.1109/melcon.2000.880372.
@article{article, author = {Blaskovic, B. and Dembitz, S. and Knezevic, P.}, editor = {Economides, C.}, year = {2000}, pages = {77-80}, DOI = {10.1109/melcon.2000.880372}, keywords = {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}, doi = {10.1109/melcon.2000.880372}, title = {Model checking of concurrent system with SDL/sup --/ specification}, keyword = {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}, publisher = {IEEE}, publisherplace = {Lemesos, Cipar} }
@article{article, author = {Blaskovic, B. and Dembitz, S. and Knezevic, P.}, editor = {Economides, C.}, year = {2000}, pages = {77-80}, DOI = {10.1109/melcon.2000.880372}, keywords = {specification languages, formal specification, formal verification, multiprocessing systems, finite state machines, reachability analysis}, doi = {10.1109/melcon.2000.880372}, title = {Model checking of concurrent system with SDL/sup --/ specification}, keyword = {specification languages, formal specification, formal verification, multiprocessing systems, finite state machines, reachability analysis}, publisher = {IEEE}, publisherplace = {Lemesos, Cipar} }

Citati:





    Contrast
    Increase Font
    Decrease Font
    Dyslexic Font