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 111
- Downloads 0
A SURVEY OF MEDICAL IMAGE PROCESSING TOOLS
A precise analysis of medical image is an important stage in the contouring phase throughout radiotherapy preparation. Medical images are mostly used as radiographic techniques in diagnosis, clinical studies and treatmen...
COMPARATIVE BENCHMARKING OF CONSTRAINTS T-WAY TEST GENERATION STRATEGY BASED ON LATE ACCEPTANCE HILL CLIMBING ALGORITHM
This paper describes the new t-way strategy based the Late Acceptance based Hill Climbing algorithm, called LAHC, for constraints t-way test generation. Unlike earlier competing work, LAHC does not require significant tu...
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...
A REVIEW OF SINGLE AND POPULATION-BASED METAHEURISTIC ALGORITHMS SOLVING MULTI DEPOT VEHICLE ROUTING PROBLEM
Multi-Depot Vehicle Routing Problem (MDVRP) arises with rapid development in the logistics and transportation field in recent years. This field, mainly, faces challenges in arranging their fleet efficiently to distribute...
DATA SECURITY ISSUES IN CLOUD COMPUTING: REVIEW
Cloud computing is an internet based model that empower on demand ease of access and pay for the usage of each access to shared pool of networks. It is yet another innovation that fulfills a client's necessity for comput...