More Web Proxy on the site http://driver.im/

research-article

Backward coverability with pruning for lossy channel systems

Authors:

Thomas Geffroy,

Jérôme Leroux,

Grégoire SutreAuthors Info & Claims

SPIN 2017: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software

Pages 132 - 141

https://doi.org/10.1145/3092282.3092292

Published: 13 July 2017 Publication History

Abstract

Driven by the concurrency revolution, the study of the coverability problem for Petri nets has regained a lot of interest in the recent years. A promising approach, which was presented in two papers last year, leverages a downward-closed forward invariant to accelerate the classical backward coverability analysis for Petri nets. In this paper, we propose a generalization of this approach to the class of well-structured transition systems (WSTSs), which contains Petri nets. We then apply this generalized approach to lossy channel systems (LCSs), a well-known subclass of WSTSs. We propose three downward-closed forward invariants for LCSs. One of them counts the number of messages in each channel, and the other two keep track of the order of messages. An experimental evaluation demonstrates the benefits of our approach.

References

[1]

P-A. Abdulla, M-F. Atig, A. Bouajjani, and T-P. Ngo. 2016. The Benefits of Duality in Verifying Concurrent Programs under TSO. In CONCUR (LIPIcs), Vol. 59. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 5:1–5:15.

[2]

P-A. Abdulla, A. Bouajjani, and B. Jonsson. 1998. On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels. In CAV (LNCS), Vol. 1427. Springer, 305–318.

Digital Library

[3]

P-A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. 2000. Algorithmic Analysis of Programs with Well Quasi-ordered Domains. Information and Computation 160, 1-2 (2000), 109–127.

Digital Library

[4]

P-A. Abdulla and B. Jonsson. 1996. Verifying Programs with Unreliable Channels. Inf. Comput. 127, 2 (1996), 91–101.

[5]

A. Annichini, A. Bouajjani, and M. Sighireanu. 2001. TReX: A Tool for Reachability Analysis of Complex Systems. In CAV (LNCS), Vol. 2102. Springer, 368–372.

Digital Library

[6]

M-F. Atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi. 2010. On the verification problem for weak memory models. In POPL. ACM, 7–18.

Digital Library

[7]

M. Blondin, A. Finkel, Ch. Haase, and S. Haddad. 2016. Approaching the Coverability Problem Continuously. In TACAS (LNCS), Vol. 9636. Springer, 480–496.

Digital Library

[8]

B. Boigelot and P. Godefroid. 1999. Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs. Formal Methods in System Design 14, 3 (1999), 237–255.

Digital Library

[9]

A. Bouajjani, P. Habermehl, and T. Vojnar. 2004. Abstract Regular Model Checking. In CAV (LNCS), Vol. 3114. Springer, 372–386.

[10]

G. Cécé, A. Finkel, and S.P. Iyer. 1996. Unreliable Channels are Easier to Verify Than Perfect Channels. Inf. Comput. 124, 1 (1996), 20–31.

Digital Library

[11]

P. Chambart and P. Schnoebelen. 2008. The Ordinal Recursive Complexity of Lossy Channel Systems. In LICS. IEEE Computer Society, 205–216.

Digital Library

[12]

E-M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. 2003. Counterexampleguided abstraction refinement for symbolic model checking. J. ACM 50, 5 (2003), 752–794.

Digital Library

[13]

P. Cousot and R. Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In POPL. ACM, 238–252.

Digital Library

[14]

L. de Moura and N. Bjørner. 2008. Z3: An Efficient SMT Solver. In TACAS (LNCS), Vol. 4963. Springer, 337–340.

Digital Library

[15]

J. Esparza, R. Ledesma-Garza, R. Majumdar, P.J. Meyer, and F. Niksic. 2014. An SMT-Based Approach to Coverability Analysis. In CAV (LNCS), Vol. 8559. Springer, 603–619.

Digital Library

[16]

A. Finkel and P. Schnoebelen. 2001. Well-structured transition systems everywhere! Theor. Comput. Sci. 256, 1-2 (2001), 63–92.

Digital Library

[17]

T. Geffroy, J. Leroux, and G. Sutre. 2016. Occam’s Razor Applied to the Petri Net Coverability Problem. In RP (LNCS), Vol. 9899. Springer, 77–89.

[18]

T. Geffroy, J. Leroux, and G. Sutre. 2017. coverability checker for LCS. http: //dept-info.labri.u-bordeaux.fr/~tgeffroy/lcs/. (2017).

[19]

A. Heußner, T. Le Gall, and G. Sutre. 2012. McScM: A General Framework for the Verification of Communicating Machines. In TACAS (LNCS), Vol. 7214. Springer, 478–484.

[20]

G. Higman. 1952. Ordering by Divisibility in Abstract Algebras. Proc. London Math. Soc. s3-2, 1 (1952), 326–336.

[21]

A. Kaiser, D. Kroening, and T. Wahl. 2014. A Widening Approach to Multithreaded Program Verification. ACM 36, 4 (2014), 14:1–14:29.

Digital Library

[22]

R. Mayr. 2003. Undecidable problems in unreliable computations. Theor. Comput. Sci. 297, 1-3 (2003), 337–354.

Digital Library

Cited By

Goubault-Larrecq JHalfon SKarandikar PNarayan Kumar KSchnoebelen P(2020)The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderingsWell-Quasi Orders in Computation, Logic, Language and Reasoning10.1007/978-3-030-30229-0_3(55-105)Online publication date: 2-Jan-2020
https://doi.org/10.1007/978-3-030-30229-0_3

Index Terms

Backward coverability with pruning for lossy channel systems
1. Theory of computation
  1. Logic
    1. Logic and verification
    2. Verification by model checking
  2. Semantics and reasoning
    1. Program reasoning
      1. Invariants
      2. Program verification

Recommendations

Nested Petri Nets — a Formalism for Specification and Verification of Multi-Agent Distributed Systems

Nested Petri nets is a formalism for modeling hierarchical multi-agent systems. Tokens in nested Petri nets are elements represented by nets themselves. Decidability of some crucial for verification problems shows that, in spite of their ”unflat” ...
Nested Petri Nets: Multi-level and Recursive Systems
Concurrency Specification and Programming (CS&P'2000)

Nested Petri nets (NP-nets) is a formalism for modeling hierarchical multi-agent systems. Tokens in nested Petri nets are elements represented by nets themselves. The paper continues investigating semantic properties of NP-nets, started in [10], where ...
Nested Petri Nets: Multi-level and Recursive Systems
Concurrency Specification and Programming (CS&P'2000)

Nested Petri nets (NP-nets) is a formalism for modeling hierarchical multi-agent systems. Tokens in nested Petri nets are elements represented by nets themselves. The paper continues investigating semantic properties of NP-nets, started in [10], where ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SPIN 2017: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software

July 2017

199 pages

ISBN:9781450350778

DOI:10.1145/3092282

Program Chairs:
Hakan Erdogmus
Carnegie Mellon University, USA
,
Klaus Havelund
NASA, USA / Jet Propulsion Laboratory, USA

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 July 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ISSTA '17

Sponsor:

SIGSOFT

ISSTA '17: International Symposium on Software Testing and Analysis

July 13 - 14, 2017

CA, Santa Barbara, USA

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
50
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)1

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Goubault-Larrecq JHalfon SKarandikar PNarayan Kumar KSchnoebelen P(2020)The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderingsWell-Quasi Orders in Computation, Logic, Language and Reasoning10.1007/978-3-030-30229-0_3(55-105)Online publication date: 2-Jan-2020
https://doi.org/10.1007/978-3-030-30229-0_3

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents