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


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


Vadym Viktorovych Shkarupylo¹*, Igor Tomičić², Kostiantyn Mykolaiovych Kasian¹ and Jamil Abedalrahim Jamil Alsayaydeh³
¹Computer Systems and Networks Dept., Zaporizhzhya National Technical University,
69063, Zhukovsky st., 64, Zaporizhzhya, Ukraine.
²Faculty of Organization and Informatics, University of Zagreb,
42000, Pavlinska, 2, Varazdin, Croatia.
³Faculty of Engineering Technology, Technical University of Malaysia Malacca
76100, Durian Tunggal, Melaka, Malaysia
E-mail: This email address is being protected from spambots. You need JavaScript enabled to view it.*, This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it., This email address is being protected from spambots. You need JavaScript enabled to view it.

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.

Keywords: TLC, TLA+, Model Checking, BFS, DFS.

pdf ico FULL PAPER
 
 
 
 
 

Contact Us

Managing Editor of IJSECS
Faculty of Computer Systems & Software Engineering (FSKKP)

Universiti Malaysia Pahang
Lebuhraya Tun Razak
26300 Gambang,
Kuantan, Pahang Darul Makmur.

Tel: +609 549 2133
Fax: +609 549 2144
Email: ijsecsfskkp@ump.edu.my

Visitor Counter

0061964
Today
Yesterday
This Week
Last Week
This Month
Last Month
All days
97
62
341
609
1205
2685
61964