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 101
- Downloads 0
Agent-Based Modelling Applied to 5D Model of the HIV Infection
This paper proposes a Multi-Agents Model to simulate the phenomenon of the infection by the Human Immunodeficiency Virus (HIV). Since the HIV was isolated in 1983 and found to be the cause of the Acquired Immune Deficien...
Technology Acceptance Model Based Study of Students’ Attitudes Toward Use of Enterprise Resource Planning Solutions
Enterprise Resource Planning (ERP) solutions are the most frequently used software tool in companies in all industries. Therefore, the labour market requires the knowledge and skills for usage of ERP solutions from gradu...
An Iterative Automatic Final Alignment Method in the Ontology Matching System
Ontology matching plays an important role in the integration of heterogeneous data sources that are described by ontologies. In order to determine correspondences between ontologies, a set of matchers can be used. After...
A Study on Knowledge Gain and Retention when Using Multimedia Learning Materials of Different Quality
The usage of multimedia has proven to foster meaningful learning, but not every multimedia resource will necessarily contribute to the teaching-learning process. Since for the development of multimedia learning materials...
The Current State and Future Perspectives of the Research Information Infrastructure in Croatia
The purpose of this paper is to analyze the existing Croatian research information infrastructure and to outline a new model of the Croatian Current Research Information System (CroRIS), required for the systematical mon...