The Investigation of TLC Model Checker Properties (CROSBI ID 226848)
Prilog u časopisu | izvorni znanstveni rad | međunarodna recenzija
Podaci o odgovornosti
Viktorovych Shkarupylo, Vadym ; Tomičić, Igor ; Mykolaiovych Kasian, Kostiantyn
engleski
The Investigation of TLC Model Checker Properties
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.
Composite Web Service ; Model Checking ; WS-BPEL ; BFS ; DFS ; TLA+ ; TLC
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o izdanju
40 (1)
2016.
145-152
objavljeno
1846-3312
1846-9418
Povezanost rada
Računarstvo