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 de...

Full description

Bibliographic Details
Main Authors:	Vadym Viktorovych Shkarupylo, Igor Tomicic, Kostiantyn Mykolaiovych Kasian
Format:	Article
Language:	English
Published:	University of Zagreb, Faculty of organization and informatics 2016-06-01
Series:	Journal of Information and Organizational Sciences
Subjects:	Composite Web Service Model Checking WS-BPEL BFS DFS TLA+ TLC
Online Access:	http://jios.foi.hr/index.php/jios/article/view/991

id	doaj-63968b5cb8464767842b5324e48bf452
record_format	Article
spelling	doaj-63968b5cb8464767842b5324e48bf4522021-09-02T01:43:41ZengUniversity of Zagreb, Faculty of organization and informaticsJournal of Information and Organizational Sciences1846-33121846-94182016-06-01401728The Investigation of TLC Model Checker PropertiesVadym Viktorovych Shkarupylo0Igor Tomicic1Kostiantyn Mykolaiovych Kasian2Computer Systems and Networks Department Zaporizhzhya National Technical University, Zaporizhzhya, UkraineUniversity of Zagreb, Faculty of Organization and InformaticsComputer Systems and Networks Department Zaporizhzhya National Technical University, Zaporizhzhya, UkraineThis 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.http://jios.foi.hr/index.php/jios/article/view/991Composite Web ServiceModel CheckingWS-BPELBFSDFSTLA+TLC
collection	DOAJ
language	English
format	Article
sources	DOAJ
author	Vadym Viktorovych Shkarupylo Igor Tomicic Kostiantyn Mykolaiovych Kasian
spellingShingle	Vadym Viktorovych Shkarupylo Igor Tomicic Kostiantyn Mykolaiovych Kasian The Investigation of TLC Model Checker Properties Journal of Information and Organizational Sciences Composite Web Service Model Checking WS-BPEL BFS DFS TLA+ TLC
author_facet	Vadym Viktorovych Shkarupylo Igor Tomicic Kostiantyn Mykolaiovych Kasian
author_sort	Vadym Viktorovych Shkarupylo
title	The Investigation of TLC Model Checker Properties
title_short	The Investigation of TLC Model Checker Properties
title_full	The Investigation of TLC Model Checker Properties
title_fullStr	The Investigation of TLC Model Checker Properties
title_full_unstemmed	The Investigation of TLC Model Checker Properties
title_sort	investigation of tlc model checker properties
publisher	University of Zagreb, Faculty of organization and informatics
series	Journal of Information and Organizational Sciences
issn	1846-3312 1846-9418
publishDate	2016-06-01
description	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.
topic	Composite Web Service Model Checking WS-BPEL BFS DFS TLA+ TLC
url	http://jios.foi.hr/index.php/jios/article/view/991
work_keys_str_mv	AT vadymviktorovychshkarupylo theinvestigationoftlcmodelcheckerproperties AT igortomicic theinvestigationoftlcmodelcheckerproperties AT kostiantynmykolaiovychkasian theinvestigationoftlcmodelcheckerproperties AT vadymviktorovychshkarupylo investigationoftlcmodelcheckerproperties AT igortomicic investigationoftlcmodelcheckerproperties AT kostiantynmykolaiovychkasian investigationoftlcmodelcheckerproperties
_version_	1721181691243921408

The Investigation of TLC Model Checker Properties

Similar Items