AN APPROACH TO INCREASE THE EFFECTIVENESS OF TLC VERIFICATION WITH RESPECT TO THE CONCURRENT STRUCTURE OF TLA+ SPECIFICATION

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

INFORMATION SYSTEMS REENGINEERING APPROACH BASED ON THE MODEL OF INFORMATION SYSTEMS DOMAINS

The paper considers current problems of integration of Information Systems (IS), limitations of current methods of IS Reengineering and limitations of existing approaches for Data Integration in Relational Databases. The...

AFRICAN BUFFALO OPTIMIZATION

This is an introductory paper to the newly-designed African Buffalo Optimization (ABO) algorithm for solving combinatorial and other optimization problems. The algorithm is inspired by the behavior of African buffalos, a...

KNOWLEDGE MAPPING PROCESS MODEL FOR RISK MITIGATION IN SOFTWARE MANAGEMENT

As software organizations try to mitigate operational and technical risk that occurs when using software, there is need to develop a knowledge intensive system to assist team members in mitigating both operational and te...

CHALLENGES OF SOFTWARE QUALITY ASSURANCE AND TESTING

Uncertainty exists in Software Company over the world. Software quality problem is leading issue for the software industry. The issue exists from 40 years or 50 years long. The industry is suffering and closing for this...

IDENTIFICATION AND QUANTIFICATION OF FACTORS AFFECTING REUSABILITY OF OPEN SOURCE SOFTWARE IN REUSE-INTENSIVE SOFTWARE DEVELOPMENT

Open Source Software (OSS) is one of the emerging areas in software engineering. Reuse of OSS is employed in reuse-intensive software development such as Component Based Software Development and Software Product Lines. O...

Download PDF file
  • EP ID EP597366
  • DOI 10.15282/ijsecs.4.1.2018.4.0037
  • Views 110
  • Downloads 0

How To Cite

Vadym Viktorovych Shkarupylo (2018). AN APPROACH TO INCREASE THE EFFECTIVENESS OF TLC VERIFICATION WITH RESPECT TO THE CONCURRENT STRUCTURE OF TLA+ SPECIFICATION. International Journal of Software Engineering and Computer Systems, 4(1), 48-60. https://europub.co.uk./articles/-A-597366