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 116
- Downloads 0
A PROPOSED FRAMEWORK TO CONTROL RUMOUR PROPAGATION ON TWITTER FOR CRITICAL NATIONAL INFORMATION INFRASTRUCTURE (CNII) ORGANISATIONS
Critical National Information Infrastructure (CNII) organisations in Malaysia consist of many crucial sectors that not solely effect on national e-sovereignty, but also on economy, social and politic matters. Due to the...
A DEVELOPED NETWORK LAYER HANDOVER BASED WIRELESS NETWORKS
This paper proposes an Advanced Mobility Handover (AMH) scheme based on Wireless Local Area Networks (WLANs) by developing a network layer handover procedure which triggers messages to be sent to the next access point. T...
LANGUAGE-AGNOSTIC SOURCE CODE RETRIEVAL USING KEYWORD & IDENTIFIER LEXICAL PATTERN
Despite the fact that source code retrieval is a promising mechanism to support software reuse, it suffers an emerging issue along with programming language development. Most of them rely on programming-language-dependen...
THE DAWN OF METAHEURISTIC ALGORITHMS
Optimization has become such a favored area of research in recent times necessitating the need for technical papers and tutorials that will properly analyze and explain the basics of the field. At the heart of efficiency...
EVALUATING THE EFFECT OF DATASET SIZE ON PREDICTIVE MODEL USING SUPERVISED LEARNING TECHNIQUE
Learning models used for prediction purposes are mostly developed without paying much cognizance to the size of datasets that can produce models of high accuracy and better generalization. Although, the general believe i...