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
- EP ID EP408269
- DOI 10.31341/jios.40.1.7
- Views 114
- Downloads 0
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...
Performance Journey Mapping: Insights from a Methodological Triangulation
This paper presents the results of an evaluation of the Performance Journey Mapping (PJM) framework. PJM is a service performance assessment concept with accompanying tools tailored to the specific performance measuremen...
From the Editor
Dear readers and authors, It is the last time I am addressing you as the editor of the Journal. From the next issue the job of the editor will be taken over by Dr. Dijana Oreški. I am sure that the new editor will bring...
Emotion-Based Content Personalization in Social Networks
Personalization is the process of customizing social network pages of users according to their needs and personal interests. It can also be used for filtering unwanted information from an individual's page received from...
Exploring Technostress: Results of a Large Sample Factor Analysis
With reference to the results of a large sample factor analysis, the article aims to propose the frame examining technostress in a population. The survey and principal component analysis of the sample consisting of 1013...