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 112
- Downloads 0
INDONESIAN TEXT-TO-SPEECH SYSTEM USING DIPHONE CONCATENATIVE SYNTHESIS
In this paper, we describe the design and develop a database of Indonesian diphone synthesis using speech segment of recorded voice to be converted from text to speech and save it as audio file like WAV or MP3. In design...
METAMODELLING APPROACH AND SOFTWARE TOOLS FOR PHYSICAL MODELLING AND SIMULATION
In computer science, metamodelling approach becomes more and more popular for the purpose of software systems development. In this paper, we discuss applicability of the metamodelling approach for development of software...
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...
CATEGORIZATION OF GELAM, ACACIA AND TUALANG HONEY ODORPROFILE USING K-NEAREST NEIGHBORS
Honey authenticity refer to honey types is of great importance issue and interest in agriculture. In current research, several documents of specific types of honey have their own usage in medical field. However, it is qu...
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...