Pregled bibliografske jedinice broj: 809683
The Investigation of TLC Model Checker Properties
The Investigation of TLC Model Checker Properties // Journal of information and organizational sciences, 40 (2016), 1; 145-152 (međunarodna recenzija, članak, znanstveni)
CROSBI ID: 809683 Za ispravke kontaktirajte CROSBI podršku putem web obrasca
Naslov
The Investigation of TLC Model Checker Properties
Autori
Viktorovych Shkarupylo, Vadym ; Tomičić, Igor ; Mykolaiovych Kasian, Kostiantyn
Izvornik
Journal of information and organizational sciences (1846-3312) 40
(2016), 1;
145-152
Vrsta, podvrsta i kategorija rada
Radovi u časopisima, članak, znanstveni
Ključne riječi
Composite Web Service ; Model Checking ; WS-BPEL ; BFS ; DFS ; TLA+ ; TLC
Sažetak
This paper presents the investigation and comparison of TLC model checking method (TLA Checker) properties. There are two different approaches to method usage which are considered. The first one consists of a transition system states attendance by breadth- first search (BFS), and the second one by depth-first search (DFS). The Kripke structure has been chosen as a transition system model. A case study has been conducted, where composite web service usage scenario has been considered. Obtained experimental results are aimed at increasing the effectiveness of TLA+ specifications automated verification.
Izvorni jezik
Engleski
Znanstvena područja
Računarstvo
POVEZANOST RADA
Ustanove:
Fakultet organizacije i informatike, Varaždin
Profili:
Igor Tomičić
(autor)
Citiraj ovu publikaciju:
Časopis indeksira:
- Web of Science Core Collection (WoSCC)
- Emerging Sources Citation Index (ESCI)
- Scopus
Uključenost u ostale bibliografske baze podataka::
- RILM: Abstracts of Music Literature Database
