Correct and Efficient Antichain Algorithms for Refinement Checking - Formal Techniques for Distributed Objects, Components, and Systems
Conference Papers Year : 2019

Correct and Efficient Antichain Algorithms for Refinement Checking

Abstract

Refinement checking plays an important role in system verification. This means that the correctness of the system is established by showing a refinement relation between two models; one for the implementation and one for the specification. In [21], Wang et al. describe an algorithm based on antichains for efficiently deciding stable failures refinement and failures-divergences refinement. We identify several issues pertaining to the correctness and performance in these algorithms and propose new, correct, antichain-based algorithms. Using a number of experiments we show that our algorithms outperform the original ones in terms of running time and memory usage.
Fichier principal
Vignette du fichier
478668_1_En_11_Chapter.pdf (512.85 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

hal-02313731 , version 1 (11-10-2019)

Licence

Identifiers

Cite

Maurice Laveaux, Jan Friso Groote, Tim Willemse. Correct and Efficient Antichain Algorithms for Refinement Checking. 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2019, Copenhagen, Denmark. pp.185-203, ⟨10.1007/978-3-030-21759-4_11⟩. ⟨hal-02313731⟩
51 View
30 Download

Altmetric

Share

More