Correct and efficient antichain algorithms for refinement checking

Maurice Laveaux; Jan Friso Groote; Tim Willemse

doi:10.1007/978-3-030-21759-4_11

Correct and efficient antichain algorithms for refinement checking

Maurice Laveaux, Jan Friso Groote, Tim Willemse

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

4 Citaten (Scopus)

Samenvatting

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.

Originele taal-2	Engels
Titel	Formal Techniques for Distributed Objects, Components, and Systems - 39th IFIP WG 6.1 International Conference, FORTE 2019, held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings
Redacteuren	Nobuko Yoshida, Jorge A. Pérez
Plaats van productie	Cham
Uitgeverij	Springer
Pagina's	185-203
Aantal pagina's	19
ISBN van elektronische versie	978-3-030-21759-4
ISBN van geprinte versie	978-3-030-21758-7
DOI's	https://doi.org/10.1007/978-3-030-21759-4_11
Status	Gepubliceerd - 29 mei 2019
Evenement	Formal Techniques for Distributed Objects, Components, and Systems: 39th IFIP WG 6.1 International Conference, FORTE 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019 - DTU Lyngby, Kongens Lyngby, Denemarken Duur: 17 jun. 2019 → 21 jun. 2019 Congresnummer: 2019 https://www.discotec.org

Publicatie series

Naam	Lecture Notes in Computer Science
Volume	11535
ISSN van geprinte versie	0302-9743
ISSN van elektronische versie	1611-3349

Congres

Congres	Formal Techniques for Distributed Objects, Components, and Systems
Verkorte titel	FORTE
Land/Regio	Denemarken
Stad	Kongens Lyngby
Periode	17/06/19 → 21/06/19
Internet adres	https://www.discotec.org

Toegang tot document

10.1007/978-3-030-21759-4_11

Andere bestanden en links

Link to publication in Scopus

Citeer dit

Laveaux, M., Groote, J. F., & Willemse, T. (2019). Correct and efficient antichain algorithms for refinement checking. In N. Yoshida, & J. A. Pérez (editors), Formal Techniques for Distributed Objects, Components, and Systems - 39th IFIP WG 6.1 International Conference, FORTE 2019, held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings (blz. 185-203). (Lecture Notes in Computer Science; Vol. 11535). Springer. https://doi.org/10.1007/978-3-030-21759-4_11

Laveaux, Maurice ; Groote, Jan Friso ; Willemse, Tim. / Correct and efficient antichain algorithms for refinement checking. Formal Techniques for Distributed Objects, Components, and Systems - 39th IFIP WG 6.1 International Conference, FORTE 2019, held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings. redacteur / Nobuko Yoshida ; Jorge A. Pérez. Cham : Springer, 2019. blz. 185-203 (Lecture Notes in Computer Science).

@inproceedings{8d54bacbc390436e82b63b488b43f85f,

title = "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{\^A} [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.",

author = "Maurice Laveaux and Groote, {Jan Friso} and Tim Willemse",

year = "2019",

month = may,

day = "29",

doi = "10.1007/978-3-030-21759-4_11",

language = "English",

isbn = "978-3-030-21758-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "185--203",

editor = "Nobuko Yoshida and P{\'e}rez, {Jorge A.}",

booktitle = "Formal Techniques for Distributed Objects, Components, and Systems - 39th IFIP WG 6.1 International Conference, FORTE 2019, held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings",

address = "Germany",

note = "Formal Techniques for Distributed Objects, Components, and Systems : 39th IFIP WG 6.1 International Conference, FORTE 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, FORTE ; Conference date: 17-06-2019 Through 21-06-2019",

url = "https://www.discotec.org",

}

Laveaux, M , Groote, JF & Willemse, T 2019, Correct and efficient antichain algorithms for refinement checking. in N Yoshida & JA Pérez (uitgave), Formal Techniques for Distributed Objects, Components, and Systems - 39th IFIP WG 6.1 International Conference, FORTE 2019, held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings. Lecture Notes in Computer Science, vol. 11535, Springer, Cham, blz. 185-203, Formal Techniques for Distributed Objects, Components, and Systems, Kongens Lyngby, Denemarken, 17/06/19. https://doi.org/10.1007/978-3-030-21759-4_11

Correct and efficient antichain algorithms for refinement checking. / Laveaux, Maurice ; Groote, Jan Friso ; Willemse, Tim.
Formal Techniques for Distributed Objects, Components, and Systems - 39th IFIP WG 6.1 International Conference, FORTE 2019, held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings. uitgave / Nobuko Yoshida; Jorge A. Pérez. Cham: Springer, 2019. blz. 185-203 (Lecture Notes in Computer Science; Vol. 11535).

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

TY - GEN

T1 - Correct and efficient antichain algorithms for refinement checking

AU - Laveaux, Maurice

AU - Groote, Jan Friso

AU - Willemse, Tim

N1 - Conference code: 2019

PY - 2019/5/29

Y1 - 2019/5/29

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85067336380&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-21759-4_11

DO - 10.1007/978-3-030-21759-4_11

M3 - Conference contribution

SN - 978-3-030-21758-7

T3 - Lecture Notes in Computer Science

SP - 185

EP - 203

BT - Formal Techniques for Distributed Objects, Components, and Systems - 39th IFIP WG 6.1 International Conference, FORTE 2019, held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings

A2 - Yoshida, Nobuko

A2 - Pérez, Jorge A.

PB - Springer

CY - Cham

T2 - Formal Techniques for Distributed Objects, Components, and Systems

Y2 - 17 June 2019 through 21 June 2019

ER -

Laveaux M , Groote JF , Willemse T. Correct and efficient antichain algorithms for refinement checking. In Yoshida N, Pérez JA, redacteurs, Formal Techniques for Distributed Objects, Components, and Systems - 39th IFIP WG 6.1 International Conference, FORTE 2019, held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings. Cham: Springer. 2019. blz. 185-203. (Lecture Notes in Computer Science). doi: 10.1007/978-3-030-21759-4_11

Correct and efficient antichain algorithms for refinement checking

Samenvatting

Publicatie series

Congres

Toegang tot document

Andere bestanden en links

Vingerafdruk

Citeer dit