article

Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems

Author:

B. JeannetAuthors Info & Claims

Formal Methods in System Design, Volume 23, Issue 1

Pages 5 - 37

https://doi.org/10.1023/A:1024480913162

Published: 01 July 2003 Publication History

Abstract

We apply linear relation analysis (P. Cousot and N. Halbwachs, in 5th ACM Symposium on Principles of Programming Languages, POPL'78 , Tucson (Arizona), January 1978; N. Halbwachs, Y.E. Proy, and P. Roumanoff, Formal Methods in System Design , Vol. 11, No. 2, pp. 157-185, 1997) to the verification of declarative synchronous programs (N. Halbwachs, Science of Computer Programming, Special Issue on SAS'94 , Vol. 31, No. 1, 1998). In this approach, state partitioning plays an important role: on one hand the precision of the results highly depends on the fineness of the partitioning; on the other hand, a too much detailed partitioning may result in an exponential explosion of the analysis. In this paper, we propose to dynamically select a suitable partitioning according to the property to be proved. The presented approach is quite general and can be applied to other abstract interpretations.

References

[1]

1. P.A. Abdulla, A. Bouajjani, and B. Jonsson, "On-the-fly analysis of systems with unbounded, lossy fifo channels," in Computer Aided Verification, CAV'98 , Vol. 1427 of LNCS, July 1998.]]

Digital Library

[2]

2. R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi, "Minimization of timed transition systems," in Proceedings of the Third Conference on Concurrency Theory CONCUR'92 , Lecture Notes in Computer Science 630, Springer-Verlag, 1992, pp. 340-354.]]

Digital Library

[3]

3. R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, "The algorithmic analysis of hybrid systems," Theoretical Computer Science B , Vol. 138, pp. 3-34, 1995.]]

Digital Library

[4]

4. G. Behrmann, K.G. Larsen, J. Pearson, C. Weise, and W. Yi, "Efficient timed reachability analysis using clock difference diagrams," in Computer Aided Verification, CAV'99 , Vol. 1633 of LNCS, July 1999.]]

Digital Library

[5]

5. S. Bensalem, Y. Lakhnech, and S. Owre, "Computing abstractions of infinite state systems compositionally and automatically," in Computer Aided Verification, CAV'98 , Vol. 1427 of LNCS, July 1998.]]

Digital Library

[6]

6. S. Bensalem, Y. Lakhnech, and H. Sadi, "Powerful techniques for the automatic generation of invariants," in Computer Aided Verification, CAV'96 , Vol. 102 of LNCS, July 1996.]]

Digital Library

[7]

7. N. Bjørner, A. Browne, and Z. Manna, "Automatic generation of invariants and intermediate assertions," Theoretical Computer Science , Vol. 173, No. 1, 1997.]]

Digital Library

[8]

8. B. Boigelot and P. Godefroid, "Symbolic verification of communication protocols with infinite state spaces using QDDs," in Computer Aided Verification, CAV'96 , Vol. 1102 of LNCS, July 1996.]]

Digital Library

[9]

9. A. Bouajjani, J.-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel, "Minimal state graph generation," Science of Computer Programming , Vol. 18, pp. 247-269, 1992.]]

Digital Library

[10]

10. A. Bouali and R. de Simone, "Symbolic bisimulation minimisation," in Computer Aided Verification, CAV'92 , Vol. 663 of LNCS, July 1992.]]

Digital Library

[11]

11. F. Bourdoncle, "Abstract interpretation by dynamic partitionning," Journal of Functional Programming , Vol. 2, No. 4, 1992.]]

[12]

12. F. Bourdoncle, "Efficient chaotic iteration strategies with widenings," in International Conference on Formal Methods in Programming and their Applications , Vol. 735 of LNCS, 1993.]]

[13]

13. E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, "Counterexample-guided abstraction refinement," in Computer Aided Verification, CAV'2000, Vol. 1855 of LNCS, July 2000.]]

Digital Library

[14]

14. M.A. Colón and T.E. Uribe, "Generating finite-state abstractions of reactive systems using decision procedures," in Computer Aided Verification, CAV'98 , Vol. 1427 of LNCS, July 1998.]]

Digital Library

[15]

15. O. Coudert, C. Berthet, and J.C. Madre, "Verification of synchronous sequential machines based on symbolic execution," in International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble . LNCS 407, Springer Verlag, 1989.]]

Digital Library

[16]

16. P. Cousot, "Asynchronous iterative methods for solving a fixpoint system of monotone equations," Technical Report IMAG-RR-88, Universit scientifique et mdicale de Grenoble, 1977.]]

[17]

17. P. Cousot and R. Cousot, "Static determination of dynamic properties of programs," in 2nd Int. Symp. on Programming . Dunod, Paris, 1976.]]

[18]

18. P. Cousot and R. Cousot, "Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints," in 4th ACM Symposium on Principles of Programming Languages, POPL'77 , Los Angeles, January 1977.]]

Digital Library

[19]

19. P. Cousot and R. Cousot, "Systematic design of program analysis frameworks," in 6th ACM Symposium on Principles of Programming Languages, POPL'79 , San Antonio, January 1979.]]

Digital Library

[20]

20. P. Cousot and R. Cousot, "Abstract interpretation frameworks," Journal of Logic and Computation , 1992.]]

[21]

21. P. Cousot and R. Cousot, "Comparing the Galois connection and widening/narrowing approaches to abstract interpretation," in M. Bruynooghe and M. Wirsing (eds.), PLILP'92 , Leuven (Belgium), LNCS 631, Springer Verlag, January 1992.]]

Digital Library

[22]

22. P. Cousot and N. Halbwachs, "Automatic discovery of linear restraints among variables of a program," in 5th ACM Symposium on Principles of Programming Languages, POPL'78 , Tucson (Arizona), January 1978.]]

Digital Library

[23]

23. C. Daws, A. Olivero, S. Tripakis, and S. Yovine, "The tool KRONOS," In Hybrid Systems III, Verification and Control , Vol. 1066 of LNCS, 1996.]]

Digital Library

[24]

24. D. Dill and H. Wong-To, "Verification of real-time systems by successive over and under approximations," in Seventh Conference on Computer-Aided Verification, CAV'95 , Lige (Belgium), LNCS 939, Springer Verlag, July 1995.]]

Digital Library

[25]

25. L. Du Bousquet, "Test fonctionnel statistique de systèmes spécifiés en LUSTRE," PhD thesis Université Joseph Fourier, Grenoble, 1999.]]

[26]

26. S. Graf and H. Saidi, "Construction of abstract state graphs with PVS," in Conference on Computer Aided Verification CAV'97, Haifa , Vol. 1254 of LNCS, June 1997.]]

Digital Library

[27]

27. N. Halbwachs, "About synchronous programming and abstract interpretation," Science of Computer Programming, Special Issue on SAS'94 , Vol. 31, No. 1, May 1998.]]

Digital Library

[28]

28. N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, "The synchronous dataflow programming language LUSTRE," Proceedings of the IEEE , Vol. 79, No. 9, pp. 1305-1320, 1991.]]

[29]

29. N. Halbwachs, F. Lagnier, and P. Raymond, "Synchronous observers and the verification of reactive systems," in M. Nivat, C. Rattray, T. Rus, and G. Scollo (Eds.), Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93 , Twente, Workshops in Computing, Springer Verlag, June 1993.]]

Digital Library

[30]

30. N. Halbwachs, Y.E. Proy, and P. Roumanoff, "Verification of real-time systems using linear relation analysis," Formal Methods in System Design , Vol. 11, No. 2, pp. 157-185, 1997.]]

Digital Library

[31]

31. T. Henzinger, P. Ho, and H. Wong-To, "HyTech: The next generation," in RTSS'95 , 1995.]]

Digital Library

[32]

32. T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model-checking for real-time systems. In LICS'92 , June 1992.]]

[33]

33. B. Jeannet, "The convex polyhedra library NEW POLKA," http://www.irisa.fr/prive/bjeannet/newpolka.html.]]

[34]

34. B. Jeannet, N. Halbwachs, and P. Raymond, "Dynamic partitioning in analyses of numerical properties," in Static Analysis Symposium, SAS'99 , Vol. 1694 of LNCS, Venezia (Italy), September 1999.]]

Digital Library

[35]

35. N.D. Jones, C. Gomard, and P. Sestoft, Partial Evaluation and Automatic Program Generation , Prentice Hall International, 1993.]]

Digital Library

[36]

36. M. Karr, "Affine relationships among variables of a program," Acta Informatica , Vol. 6, pp. 133-151, 1976.]]

Digital Library

[37]

37. F. Larsson, K.G. Larsen, P. Pettersson, and W. Yi, "Efficient verification of real-time systems: Compact data structures and state-space reduction," in Proc. of the 18th IEEE Real-Time Systems Symposium . IEEE Computer Society Press, December 1997.]]

Digital Library

[38]

38. K.G. Larsen, P. Pettersson, and W. Yi, "UPPAAL in a nutshell," Springer International Journal of Software Tools for Technology Transfer , Vol. 1, Nos. (1/2), 1997.]]

[39]

39. P. LeGuernic, T. Gautier, M. LeBorgne, and C. LeMaire, "Programming real time applications with SIGNAL," Proceedings of the IEEE , Vol. 79, No. 9, pp. 1321-1336, 1991.]]

[40]

40. C. Mauras, "Calcul symbolique et automates interprétés," Technical Report 10, IRCyN, November 1996.]]

[41]

41. A. Miné, "Représentation d'ensembles de contraintes de somme ou de différence de deux variables et applicationà l'analyse automatique de programmes," Master's thesis, Laboratoire d'Informatique de l'École Normale Supérieure de Paris, July 2000.]]

[42]

42. J. Møller, J. Lichtenberg, H.R. Andersen, and H. Hulgaard, "Difference decision diagrams," in Computer Science Logic , The IT University of Copenhagen, Denmark, September 1999.]]

Digital Library

[43]

43. C. Ratel, N. Halbwachs, and P. Raymond, "Programming and verifying critical systems by means of the synchronous data-flow programming language LUSTRE," in ACM-SIGSOFT'91 Conference on Software for Critical Systems , New Orleans, December 1991.]]

Digital Library

[44]

44. P. Raymond, "Compilation efficace d'un langage déclaratif synchrone: Le générateur de code LUSTRE-V3," PhD thesis, Institut National Polytechnique de Grenoble, November 1991.]]

[45]

45. H. Sipma, T.E. Uribe, and Z. Manna, "Deductive model checking," in 8th International Conference on Computer Aided Verification, CAV'96 , Vol. 1102 of LNCS, July 1996.]]

Digital Library

[46]

46. F. Somenzi, "CUDD: Colorado University decision diagram package," ftp://vlsi.colorado.edu/pub.]]

[47]

47. R.F.L. Spelberg, W.J. Toetenel, and M. Ammerlaan, "Partition refinement in real-time model checking," in 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems , LNCS 1486, Springer Verlag, 1998, pp. 143-157.]]

Digital Library

[48]

48. The Caml language, http://caml.inria.fr/.]]

[49]

49. M. Yanakakis and D. Lee, "An efficient algorithm for minimizing real-time transition systems," in Fifth Conference on Computer-Aided Verification, CAV'93 , Elounda (Greece), LNCS 697, Springer Verlag, July 1993.]]

Digital Library

Cited By

Tokariev PMallet F(2024)Real-Time CCSL: Application to the Mechanical Lung VentilatorRigorous State-Based Methods10.1007/978-3-031-63790-2_24(289-306)Online publication date: 25-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-63790-2_24
De Maria EBahrami AL’Yvonnet TFelty AGaffé DRessouche AGrammont F(2022)On the use of formal methods to model and verify neuronal archetypesFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-020-0029-616:3Online publication date: 1-Jun-2022
https://dl.acm.org/doi/10.1007/s11704-020-0029-6
Winkler TLehmann JKatoen J(2022)Out of Control: Reducing Probabilistic Models by Control-State EliminationVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-94583-1_22(450-472)Online publication date: 16-Jan-2022
https://dl.acm.org/doi/10.1007/978-3-030-94583-1_22
Show More Cited By

Index Terms

Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems

Recommendations

Abstract acceleration in linear relation analysis

Linear relation analysis is a classical abstract interpretation based on an over-approximation of reachable numerical states of a program by convex polyhedra. Since it works with a lattice of infinite height, it makes use of a widening operator to ...
Pushdown control-flow analysis for free
POPL '16

Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Precise and efficient static array bound checking for large embedded C programs
PLDI '04

In this paper we describe the design and implementation of a static array-bound checker for a family of embedded programs: the flight control software of recent Mars missions. These codes are large (up to 280 KLOC), pointer intensive, heavily ...

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 23, Issue 1

July 2003

102 pages

ISSN:0925-9856

Issue’s Table of Contents

Copyright © Copyright © 2003 Kluwer Academic Publishers.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 July 2003

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

33
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Tokariev PMallet F(2024)Real-Time CCSL: Application to the Mechanical Lung VentilatorRigorous State-Based Methods10.1007/978-3-031-63790-2_24(289-306)Online publication date: 25-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-63790-2_24
De Maria EBahrami AL’Yvonnet TFelty AGaffé DRessouche AGrammont F(2022)On the use of formal methods to model and verify neuronal archetypesFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-020-0029-616:3Online publication date: 1-Jun-2022
https://dl.acm.org/doi/10.1007/s11704-020-0029-6
Winkler TLehmann JKatoen J(2022)Out of Control: Reducing Probabilistic Models by Control-State EliminationVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-94583-1_22(450-472)Online publication date: 16-Jan-2022
https://dl.acm.org/doi/10.1007/978-3-030-94583-1_22
Yin BChen LLiu JWang JCousot P(2019)Verifying Numerical Programs via Iterative Abstract TestingStatic Analysis10.1007/978-3-030-32304-2_13(247-267)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-32304-2_13
Giet JMauborgne LKästner DFerdinand C(2019)Towards Zero Alarms in Sound Static Analysis of Finite State MachinesComputer Safety, Reliability, and Security10.1007/978-3-030-26601-1_1(3-18)Online publication date: 10-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-26601-1_1
Kim SRival XRyu S(2018)A Theoretical Foundation of Sensitivity in an Abstract Interpretation FrameworkACM Transactions on Programming Languages and Systems10.1145/323062440:3(1-44)Online publication date: 9-Aug-2018
https://dl.acm.org/doi/10.1145/3230624
Miné A(2017)Tutorial on Static Inference of Numeric Invariants by Abstract InterpretationFoundations and Trends in Programming Languages10.1561/25000000344:3-4(120-372)Online publication date: 5-Dec-2017
https://dl.acm.org/doi/10.1561/2500000034
De Maria EL'Yvonnet TGaffé DRessouche AGrammont F(2017)Modelling and Formal Verification of Neuronal Archetypes CouplingProceedings of the 8th International Conference on Computational Systems-Biology and Bioinformatics10.1145/3156346.3156348(3-10)Online publication date: 7-Dec-2017
https://dl.acm.org/doi/10.1145/3156346.3156348
Altisen KMoy M(2016)Causality problem in real-time calculusFormal Methods in System Design10.1007/s10703-016-0250-y48:1-2(1-45)Online publication date: 1-Apr-2016
https://dl.acm.org/doi/10.1007/s10703-016-0250-y
Petrenko ATimo ORamesh S(2015)Model-based testing of automotive softwareProceedings of the 52nd Annual Design Automation Conference10.1145/2744769.2747935(1-6)Online publication date: 7-Jun-2015
https://dl.acm.org/doi/10.1145/2744769.2747935
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents