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 99
- Downloads 0
A Study on Recommendation Systems in Location Based Social Networking
Smart devices in the hands of people are revolutionizing the social lifestyle of one's self. Everyone across the world are using smart devices linked to their social networking activities one such activity is to share lo...
Using AHP Method for Making a Decision on How the Management of Sewage Sludge in the Northern Croatia
By 2018, in Croatia, the agglomerations for collecting the sewage and water treatment systems are going to be constructed. All devices will be based on the mechanical-biological method of purification. However, the work...
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...
Methods and Algorithms of Alternatives Ranging in Managing the Telecommunication Services Quality
The article deals with methods of solving the problem of ranging of alternatives in information-analytical system of managing the quality of telecommunication services rendering process. Tasks of choice are determined, i...
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...