AN APPROACH TO INCREASE THE EFFECTIVENESS OF TLC VERIFICATION WITH RESPECT TO THE CONCURRENT STRUCTURE OF TLA+ SPECIFICATION
Journal Title: International Journal of Software Engineering and Computer Systems - Year 2018, Vol 4, Issue 1
Abstract
Modern approaches to distributed software systems engineering are tightly bounded with formal methods usage. The effective way of certain method application can leverage significant outcome, in terms of corresponding time costs reduction for instance. To this end the TLC model checker has been considered – with respect to TLA+ specifications with concurrent structure. The concurrency itself has been implemented as interleaving. Two different approaches to TLC model checking have been used. The first approach is based on model checking via breadth-first state space search (BFS), the second one – via depth-first search (DFS). The main result of a paper is the new approach to increasing the effectiveness of TLC verification with respect to the concurrent structure of TLA+ specification. To analytically represent synthesized TLA+ specifications with concurrent structure, the Kripke structure has been taken. To assess the measures of state space explosion problem, taking place during the experimentation, the appropriate estimations have been proposed. These estimations have been proved during the case study. The composite web service usage scenario has been considered as a case study. The results, obtained during the experimentation, can be used to increase the effectiveness of automated TLC verification with respect to the concurrent structure of TLA+ specification.
Authors and Affiliations
Vadym Viktorovych Shkarupylo
Keywords
Related Articles
- EP ID EP597366
- DOI 10.15282/ijsecs.4.1.2018.4.0037
- Views 102
- Downloads 0
MULTI-FACTOR ATTENDANCE AUTHENTICATION SYSTEM
Taking attendance in classes is a cumbersome task which can benefit from smartphone innovation. This study identifies the vulnerabilities of the technology and proposes a technique to identify cheating. Several smartphon...
A MODIFIED ROUTE DISCOVERY APPROACH FOR DYNAMIC SOURCE ROUTING (DSR) PROTOCOL IN MOBILE AD-HOC NETWORKS
Mobile Ad-hoc networks (MANETs) involved in many applications, whether commercial or military because of their characteristics that do not depend on the infrastructure as well as the freedom movement of their elements, b...
REPRESENTING VARIABILITY IN SOFTWARE ARCHITECTURE: A SYSTEMATIC LITERATURE REVIEW
Variability in software-intensive systems is the ability of a software artefact (e.g., a system, subsystem, or component) to be extended, customised or configured for deployment in a specific context. Software Architectu...
PARAMETER-LESS SIMULATED KALMAN FILTER
Simulated Kalman Filter (SKF) algorithm is a new population-based metaheuristic optimization algorithm. In the original SKF algorithm, three parameter values are assigned during initialization, the initial error covarian...
PARALLEL INTEGRATION ALGORITHM AND ITS USAGE FOR A PRACTICAL SIMULATION OF SPACECRAFT ATTITUDE MOTION
Nowadays multi-core processors are installed almost in each modern workstation, but the question of these computational resources effective utilization is still a topical one. In this paper the four-point block one-step...