Nalazite se na CroRIS probnoj okolini. Ovdje evidentirani podaci neće biti pohranjeni u Informacijskom sustavu znanosti RH. Ako je ovo greška, CroRIS produkcijskoj okolini moguće je pristupi putem poveznice www.croris.hr
izvor podataka: crosbi

An approach to increase the effectiveness of TLC verification with respect to the concurrent structure of TLA+ specification (CROSBI ID 249170)

Prilog u časopisu | izvorni znanstveni rad | međunarodna recenzija

Viktorovych Shkarupylo, Vadym ; Tomičić, Igor ; Mykolaiovych Kasian, Kostiantyn ; Abedalrahim Jamil Alsayaydeh, Jamil An approach to increase the effectiveness of TLC verification with respect to the concurrent structure of TLA+ specification // International journal of software engineering and computer systems (Pahang), 4 (2018), 1; 48-60. doi: 10.15282/ijsecs.4.1.2018.4.0037

Podaci o odgovornosti

Viktorovych Shkarupylo, Vadym ; Tomičić, Igor ; Mykolaiovych Kasian, Kostiantyn ; Abedalrahim Jamil Alsayaydeh, Jamil

engleski

An approach to increase the effectiveness of TLC verification with respect to the concurrent structure of TLA+ specification

Modern approaches to distributed software systems engineering are tightly bounded with formal methods usage. The effective way of certain method application can leverage significant outcome, in terms of corresponding time costs reduction for instance. To this end the TLC model checker has been considered – with respect to TLA+ specifications with concurrent structure. The concurrency itself has been implemented as interleaving. Two different approaches to TLC model checking have been used. The first approach is based on model checking via breadth-first state space search (BFS), the second one – via depth-first search (DFS). The main result of a paper is the new approach to increasing the effectiveness of TLC verification with respect to the concurrent structure of TLA+ specification. To analytically represent synthesized TLA+ specifications with concurrent structure, the Kripke structure has been taken. To assess the measures of state space explosion problem, taking place during the experimentation, the appropriate estimations have been proposed. These estimations have been proved during the case study. The composite web service usage scenario has been considered as a case study. The results, obtained during the experimentation, can be used to increase the effectiveness of automated TLC verification with respect to the concurrent structure of TLA+ specification.

TLC ; TLA+ ; model checking ; BFS ; DFS

nije evidentirano

nije evidentirano

nije evidentirano

nije evidentirano

nije evidentirano

nije evidentirano

Podaci o izdanju

4 (1)

2018.

48-60

objavljeno

2889-8522

2180-0650

10.15282/ijsecs.4.1.2018.4.0037

Povezanost rada

Računarstvo

Poveznice