The Investigation of TLC Model Checker Properties

Authors

  • Vadym Viktorovych Shkarupylo Computer Systems and Networks Department Zaporizhzhya National Technical University, Zaporizhzhya, Ukraine
  • Igor Tomicic University of Zagreb, Faculty of Organization and Informatics
  • Kostiantyn Mykolaiovych Kasian Computer Systems and Networks Department Zaporizhzhya National Technical University, Zaporizhzhya, Ukraine

DOI:

https://doi.org/10.31341/jios.40.1.7

Keywords:

Composite Web Service, Model Checking, WS-BPEL, BFS, DFS, TLA , TLC

Abstract

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.

Downloads

Published

2016-06-16

How to Cite

[1]
V. Viktorovych Shkarupylo, I. Tomicic, and K. Mykolaiovych Kasian, “The Investigation of TLC Model Checker Properties”, J. inf. organ. sci. (Online), vol. 40, no. 1, Jun. 2016.

Issue

Vol. 40 No. 1 (2016)

Section

Articles