The Investigation of TLC Model Checker Properties

Journal Title: Journal of Information and Organizational Sciences - Year 2016, Vol 40, Issue 1

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.

Authors and Affiliations

Vadym Viktorovych Shkarupylo, Igor Tomičić, Kostiantyn Mykolaiovych Kasian

Keywords

Related Articles

Individual Entrepreneurial Behavior in Croatian IT Firms: The Contribution of Strategic Thinking Skills

This article addresses the contribution of strategic thinking skills in explaining individual entrepreneurial behavior in Croatian IT firms. Strategic thinking skills were assessed according to entrepreneurs’ use of syst...

A Guidance Based Approach for Enhancing the e-Government Interoperability

Developing e-Government interoperability in the government context is a complex task. As interoperability in government context is associated and hindered by many challenges and barriers connected to government nature of...

Beyond Knowledge Integration Barriers in ERP Implementations: An Institutional Approach

The objective of the article is to go beyond the knowledge integration barriers in ERP implementations by analyzing structural, technological, intellectual and socioemotional barriers that appear during an ERP implementa...

Knowledge Management Systems in the Polish Private, State and Foreign Owned Companies

The importance of knowledge management for enterprises increased significantly in the recent years. In this paper one element of knowledge management will be considered, namely knowledge management systems (KMS). The mai...

Enhancing Formal Methods Integration with ACP2Petri

The paper deals with the ACP2Petri tool, providing a transformation of process algebraic specification to equivalent Petri net-based specification. Long-term practical experiences with the tool revealed some suggestions...

Download PDF file
  • EP ID EP408269
  • DOI 10.31341/jios.40.1.7
  • Views 116
  • Downloads 0

How To Cite

Vadym Viktorovych Shkarupylo, Igor Tomičić, Kostiantyn Mykolaiovych Kasian (2016). The Investigation of TLC Model Checker Properties. Journal of Information and Organizational Sciences, 40(1), 145-152. https://europub.co.uk/articles/-A-408269