Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-02313731
Contributor : Hal Ifip <>
Submitted on : Friday, October 11, 2019 - 2:55:05 PM
Last modification on : Friday, October 11, 2019 - 3:43:39 PM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2022-01-01

Please log in to resquest access to the document

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Maurice Laveaux, Jan 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⟩

Share

Metrics

Record views

40