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

article

Using Forward Reachability Analysis for Verification of Lossy Channel Systems

Authors:

Parosh Aziz Abdulla,

Aurore Collomb-Annichini,

Ahmed Bouajjani,

Bengt JonssonAuthors Info & Claims

Formal Methods in System Design, Volume 25, Issue 1

Pages 39 - 65

https://doi.org/10.1023/B:FORM.0000033962.51898.1a

Published: 01 July 2004 Publication History

Abstract

We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for computing (i) inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop. All these operations are rather simple and can be carried out in polynomial time.

With these techniques, one can straightforwardly construct an algorithm which explores the set of reachable states of a protocol, in order to check various safety properties. We also show how one can perform model-checking of LTL properties, using a standard automata-theoretic construction. It should be noted that all these methods are by necessity incomplete, even for the class of protocols with lossy channels.

To illustrate the applicability of our methods, we have developed a tool prototype and used the tool for automatic verification of (a parameterized version of) the Bounded Retransmission Protocol.

References

[1]

1. Parosh Aziz Abdulla and Bengt Jonsson, "Undecidable verification problems for programs with unreliable channels," Information and Computation, Vol. 130, No. 1, pp. 71-90, 1996.]]

Digital Library

[2]

2. Parosh Aziz Abdulla and Bengt Jonsson, "Verifying programs with unreliable channels," Information and Computation, Vol. 127, No. 2, pp. 91-101, 1996.]]

[3]

3. A. Annichini, A. Bouajjani, and M. Sighireanu, "TReX: A tool for reachability analysis of complex systems," in Proc. 13th Intern. Conf. on Computer Aided Verification (CAV'01), Paris, France, July 2001. Lecture Notes in Computer Science 2102, Springer-Verlag.]]

Digital Library

[4]

4. S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis, "Property-preserving simulations," in CAV'92. LNCS 663, 1992.]]

Digital Library

[5]

5. S. Bensalem, Y. Lakhnech, and S. Owre, "Invest: A tool for the verification of invariants," in Computer Aided Verification, Alan J. Hu and Moshe Y. Vardi (Eds.), Vol. 1427 of Lecture Notes in Computer Science, Springer-Verlag, 1998, pp. 505-510.]]

Digital Library

[6]

6. G.V. Bochman, "Finite state description of communicating protocols," Computer Networks, Vol. 2, pp. 361- 371, 1978.]]

[7]

7. B. Boigelot and P. Godefroid, "Symbolic verification of communication protocols with infinite state spaces using QDDs," in Proc. 8th Int. Conf. on Computer Aided Verification, Alur and Henzinger (Eds.), Vol. 1102 of Lecture Notes in Computer Science, Springer Verlag, 1996, pp. 1-12.]]

Digital Library

[8]

8. B. Boigelot, P. Godefroid, B. Willems, and P. Wolper, "The power of QDDs," Available at http://www.montefiore.ulg.ac.be/~biogelot/research/BGWW97.ps.]]

[9]

9. B. Boigelot, P. Godefroid, B. Willems, and P. Wolper, "The power of QDDs," in Proc. of the Fourth International Static Analysis Symposium, Lecture Notes in Computer Science. Springer Verlag, 1997.]]

Digital Library

[10]

10. B. Boigelot and P. Wolper, "Symbolic verification with periodic sets," in Proc. 6th Int. Conf. on Computer Aided Verification, Vol. 818 of Lecture Notes in Computer Science, Springer Verlag, 1994, pp. 55- 67.]]

Digital Library

[11]

11. A. Bouajjani and P. Habermehl, "Symbolic reachability analysis of fifo-channel systems with nonregular sets of configurations," http://www.imag.fr/VERIMAG/PEOPLE/Peter.Habermehl.]]

[12]

12. A. Bouajjani and P. Habermehl, "Symbolic reachability analysis of Fifo-Channel Systems with Nonregular Sets of Configurations," Theoretical Computer Science, Vol. 221, Nos. 1/2, 1999.]]

Digital Library

[13]

13. D. Brand and P. Zafiropulo, "On communicating finite-state machines," Journal of the ACM, Vol. 2, No. 5, pp. 323-342, 1983.]]

Digital Library

[14]

14. Gérard Cécé, Alain Finkel, and S. Purushothaman Iyer, "Unreliable channels are easier to verify than perfect channels," Information and Computation, Vol. 124, No. 1, pp. 20-31, 1996.]]

Digital Library

[15]

15. A. Choquet and A. Finkel, "Simulation of linear FIFO nets having a structured set of terminal markings," in Proc. 8th European Workshop on Applications and Theory of Petri Nets, 1987.]]

[16]

16. C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis, "Memory efficient algorithms for the verification of temporal properties," in Proc. Workshop on Computer Aided Verification, 1990.]]

Digital Library

[17]

17. P. D'Argenio, J.-P. Katoen, T. Ruys, and G.J. Tretmans, "The bounded retransmission protocol must be on time," in TACAS'97. LNCS 1217, 1997.]]

Digital Library

[18]

18. J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu, "CADP: A protocol validation and verification toolbox," in CAV'96. LNCS 1102, 1996.]]

Digital Library

[19]

19. J.Cl. Fernandez and L. Mounier, "A tool set for deciding behavioural equivalences," in CONCUR'91. LNCS 527, 1991.]]

Digital Library

[20]

20. A. Finkel and O. Marcé, "Verification of infinite regular communicating automata," Technical report, LIFAC, Ecole Normale Supérieure de Cachan, Technical Report, 1996.]]

[21]

21. M.G. Gouda, E.M. Gurari, T.-H. Lai, and L.E. Rosier, "On deadlock detection in systems of communicating finite state machines," Computers and Artificial Intelligence, Vol. 6, No. 3, pp. 209-228, 1987.]]

Digital Library

[22]

22. S. Graf and H. Saidi, "Construction of abstract state graphs with PVS," in Proc. 9th Int. Conf. on Computer Aided Verification, Vol. 1254, Haifa, Israel, Springer Verlag, 1997.]]

Digital Library

[23]

23. J.F. Groote and J. van de Pol, "A bounded retransmission protocol for large data packets," Technical report, Department of Philosophy, Utrecht University, Oct. 1993.]]

[24]

24. O. Grumberg and D.E. Long, "Model checking and modular verification," in Proc. CONCUR '91, Theories of Concurrency: Unification and Extension, J.C.M. Baseten and J.F. Groote (Eds.), Vol. 527 of Lecture Notes in Computer Science, Amsterdam, Holland, Springer Verlag, 1991, pp. 250-265.]]

Digital Library

[25]

25. K. Havelund and N. Shankar, "Experiments in theorem proving and model checking for protocol verification," in FME'96. LNCS 1051, 1996.]]

Digital Library

[26]

26. L. Helmink, M.P.A. Sellink, and F. Vaandrager, "Proof checking a data link protocol," in Types for Proofs and Programs. LNCS 806, 1994.]]

Digital Library

[27]

27. G. Higman, "Ordering by divisibility in abstract algebras," Proc. London Math. Soc., Vol. 2, pp. 326-336, 1952.]]

[28]

28. G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.]]

Digital Library

[29]

29. R. Mateescu, "Formal description and analysis of a bounded retransmission protocol," Technical report no. 2965, INRIA, 1996.]]

[30]

30. R. Mayr, "Undecidable problems in unreliable computations," in Theoretical Informatics (LATIN'2000), number 1776 in Lecture Notes in Computer Science, 2000.]]

Digital Library

[31]

31. J.K. Pachl, "Protocol description and analysis based on a state transition model with channel expressions," in Protocol Specification, Testing, and Verification VII, May 1987.]]

Digital Library

[32]

32. W. Peng and S. Purushothaman, "Data flow analysis of communicating finite state machines," ACM Trans. on Programming Languages and Systems, Vol. 13, No. 3, pp. 399-442, 1991.]]

Digital Library

[33]

33. A.P. Sistla and L.D. Zuck, "Automafic temporal verification of buffer systems," in Proc. Workshop on Computer Aided Verification, Larsen and Skou (Eds.), Vol. 575 of Lecture Notes in Computer Science, Springer Verlag, 1991.]]

Digital Library

[34]

34. M.Y. Vardi and P. Wolper, "An automata-theoretic approach to automatic program verification," in Proc. LICS '86, 1st IEEE Int. Symp. on Logic in Computer Science, June 1986, pp. 332-344.]]

Cited By

Martens WLibkin LBarceló P(2022)Towards Theory for Real-World DataProceedings of the 41st ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems10.1145/3517804.3526066(261-276)Online publication date: 12-Jun-2022
https://dl.acm.org/doi/10.1145/3517804.3526066
Lingg Jde Oliveira Oliveira MWolf P(2022)Learning from Positive and Negative Examples: Dichotomies and Parameterized AlgorithmsCombinatorial Algorithms10.1007/978-3-031-06678-8_29(398-411)Online publication date: 7-Jun-2022
https://dl.acm.org/doi/10.1007/978-3-031-06678-8_29
Köcher C(2021)Reachability Problems on Reliable and Lossy Queue AutomataTheory of Computing Systems10.1007/s00224-021-10031-265:8(1211-1242)Online publication date: 1-Nov-2021
https://dl.acm.org/doi/10.1007/s00224-021-10031-2
Show More Cited By

Index Terms

Using Forward Reachability Analysis for Verification of Lossy Channel Systems

Recommendations

Using forward reachability analysis for verification of timed petri nets

We consider verification of safety properties for concurrent real-timed systems modelled as timed Petri nets by performing symbolic forward reachability analysis. We introduce a formalism, called region generators, for representing sets of markings of ...
Compositional reachability analysis for efficient modular verification of asynchronous designs

Compositional verification is essential to address state explosion in model checking. Traditionally, an over-approximate context is needed for each individual component in a system for sound verification. This may cause state explosion for the ...
Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Methods in System Design

Formal Methods in System Design Volume 25, Issue 1

July 2004

91 pages

ISSN:0925-9856

Issue’s Table of Contents

Copyright © Copyright © 2004 Kluwer Academic Publishers.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 July 2004

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

36
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 17 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Martens WLibkin LBarceló P(2022)Towards Theory for Real-World DataProceedings of the 41st ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems10.1145/3517804.3526066(261-276)Online publication date: 12-Jun-2022
https://dl.acm.org/doi/10.1145/3517804.3526066
Lingg Jde Oliveira Oliveira MWolf P(2022)Learning from Positive and Negative Examples: Dichotomies and Parameterized AlgorithmsCombinatorial Algorithms10.1007/978-3-031-06678-8_29(398-411)Online publication date: 7-Jun-2022
https://dl.acm.org/doi/10.1007/978-3-031-06678-8_29
Köcher C(2021)Reachability Problems on Reliable and Lossy Queue AutomataTheory of Computing Systems10.1007/s00224-021-10031-265:8(1211-1242)Online publication date: 1-Nov-2021
https://dl.acm.org/doi/10.1007/s00224-021-10031-2
Köcher C(2019)Reachability Problems on Partially Lossy Queue AutomataReachability Problems10.1007/978-3-030-30806-3_12(149-163)Online publication date: 11-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-30806-3_12
Hampson C(2019)On the Termination Problem for Counter Machines with Incrementing ErrorsReachability Problems10.1007/978-3-030-30806-3_11(137-148)Online publication date: 11-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-30806-3_11
Halfon SSchnoebelen PZetzsche GAceto LIngólfsdóttir A(2017)Decidability, complexity, and expressiveness of first-order logic over the subword orderingProceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3329995.3330076(1-12)Online publication date: 20-Jun-2017
https://dl.acm.org/doi/10.5555/3329995.3330076
Drăgoi CHenzinger TZufferey D(2016)PSync: a partially synchronous language for fault-tolerant distributed algorithmsACM SIGPLAN Notices10.1145/2914770.283765051:1(400-415)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837650
Lazić ROuaknine JWorrell J(2016)Zeno, Hercules, and the HydraACM Transactions on Computational Logic10.1145/287477417:3(1-27)Online publication date: 17-Feb-2016
https://dl.acm.org/doi/10.1145/2874774
Drăgoi CHenzinger TZufferey DBodik RMajumdar R(2016)PSync: a partially synchronous language for fault-tolerant distributed algorithmsProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2837614.2837650(400-415)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2837614.2837650
(2016)Forward analysis and model checking for trace bounded WSTSTheoretical Computer Science10.1016/j.tcs.2016.04.020637:C(1-29)Online publication date: 18-Jul-2016
https://dl.acm.org/doi/10.1016/j.tcs.2016.04.020
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents