×

A global constraint for over-approximation of real-time streams. (English) Zbl 1387.90206

Summary: Formal verification of real time programs, where variables can change values at every time step, is difficult due to the analyses of loops with time lags. In this paper, we propose a constraint programming model together with a global constraint and a filtering algorithm, for computing over-approximation of real-time streams. The global constraint handles the loop analyses by providing an interval over-approximation of the loop invariant. We apply our method to the FAUST language, a language for processing real-time audio streams. Experiments show that our approach provides accurate results in short times.

MSC:

90C27 Combinatorial optimization

Software:

LUSTRE
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Apt, K.R. (1999). The essence of constraint propagation. Theoretical Computer Science, 221(1-2), 179-210. · Zbl 0930.68164 · doi:10.1016/S0304-3975(99)00032-8
[2] Araya, I., Trombettoni, G., Neveu, B., & Chabert, G. Upper Bounding in Inner Regions for Global Optimization under Inequality Constraints. Journal of Global Optimization (2), 145-164 (2014). · Zbl 1312.90057
[3] Bart, A.; Truchet, C.; Monfroy, E., Verifying a real-time language with constraints (2015)
[4] Benhamou, F.; Granvilliers, L., Continuous and interval constraints, 571-603 (2006) · doi:10.1016/S1574-6526(06)80020-9
[5] Benhamou, F., & J. Older, W. (1997). Applying interval arithmetic to real, integer and Boolean constraints. Journal of Logic Programming, 32(1), 1-24. · Zbl 0882.68032 · doi:10.1016/S0743-1066(96)00142-2
[6] Blanc, B., Junke, C., Marre, B., Gall, P.L., & Andrieu, O. (2010). Handling state-machines specifications with gatel. Electronic Notes in Theoretical Computer Science, 264(3), 3-17. · doi:10.1016/j.entcs.2010.12.011
[7] Bygde, S.; Ermedahl, A.; Lisper, B., An efficient algorithm for parametric WCET calculation, 13-21 (2009)
[8] Chabert, G., & Jaulin, L. (2009). Contractor programming. Artificial Intelligence, 173(11), 1079-1100. · Zbl 1191.68628 · doi:10.1016/j.artint.2009.03.002
[9] Collavizza, H., Delobel, F., & Rueher, M. (1998). A note on partial consistencies over continuous domains (pp. 147-161). Berlin: Springer. · Zbl 0949.68100
[10] Collavizza, H.; Michel, C.; Ponsini, O.; Rueher, M., Generating test cases inside suspicious intervals for floating-point number programs, 7-11 (2014), New York · doi:10.1145/2593735.2593737
[11] Cousot, P.; Cousot, R., Static determination of dynamic properties of programs, 106-130 (1976), Paris · Zbl 0788.68094
[12] Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, 238-252 (1977), New York, Los Angeles
[13] Cousot, P., & Cousot, R. (1992). Abstract interpretation frameworks. Journal of Logic and Computation, 2(4), 511-547. · Zbl 0783.68073 · doi:10.1093/logcom/2.4.511
[14] Denmat, T.; Gotlieb, A.; Ducassé, M., An abstract interpretation based combinator for modeling while loops in constraint programming, 241-255 (2007) · Zbl 1145.68510
[15] Di Alesio, S.; Nejati, S.; Briand, LC; Gotlieb, A., Worst-case scheduling of software tasks - a constraint optimization model to support performance testing (2014)
[16] Edgar Moore, R. (1966). Interval analysis. Englewood Cliffs: Prentice-Hall.
[17] Gotlieb, A. (2015). Constraint-based testing: An emerging trend in software testing. Advances in Computers, 99, 67-101. · doi:10.1016/bs.adcom.2015.05.002
[18] Halbwachs, N., Caspi, P., Raymond, P., & Pilaud, D. (1991). The synchronous dataflow programming language lustre. Proceedings of the IEEE, 79(9), 1305-1320. · doi:10.1109/5.97300
[19] Lallouet, A.; Law, YC; Lee, JH; Siu, CF, Constraint programming on infinite data streams (2011)
[20] Lee, B.; Resnick, K.; Bond, MD; McKinley, KS, Compiler construction: 16th international conference, CC 2007, held as part of the joint European conferences on theory and practice of software, ETAPS 2007, Braga, Portugal, March 26-30, 2007, 80-95 (2007), Berlin
[21] Lee, J., & Lee, J. In: Principles and Practice of Constraint Programming. · Zbl 1222.68013
[22] Lhomme, O. (1993). Consistency techniques for numeric csps (pp. 232-238). · Zbl 0284.68074
[23] (2013). moForte: audio modeling for mobile. http://www.moforte.com.
[24] Montanari, U. (1974). Networks of constraints: fundamental properties and applications to picture processing. Information Science, 7(2), 95-132. · Zbl 0284.68074 · doi:10.1016/0020-0255(74)90008-5
[25] Oppenheim, A.V., Willsky, A.S., & Nawab, S.H. (1996). Signals & systems, 2nd Edn. Upper Saddle River: Prentice-Hall.
[26] Orlarey, Y.; Fober, D.; Letz, S., An algebra for block diagram languages (2002)
[27] Orlarey, Y., Fober, D., & Letz, S. (2004). Syntactical and semantical aspects of Faust. Soft Computing, 8(9), 623-632. · Zbl 1063.68693 · doi:10.1007/s00500-004-0388-1
[28] Pelleau, M.; Miné, A.; Truchet, C.; Benhamou, F., A constraint solver based on abstract domains, 434-454 (2013) · Zbl 1426.68159
[29] Podelski, A. (2000). chap. Model checking as constraint solving. In Proceedings of the static analysis: 7th international symposium, SAS 2000, Santa Barbara, CA, USA, June 29 - July 1, 2000 (pp. 22-37). Berlin: Springer. · Zbl 0966.68121
[30] Ponsini, O., Michel, C., & Rueher, M. (2011). Refining Abstract Interpretation-based Approximations with Constraint Solvers. Tech. rep.
[31] Ponsini, O., Michel, C., & Rueher, M. (2016). Verifying floating-point programs with constraint programming and abstract interpretation techniques. Automated Software Engineering, 23(2), 191-217. · doi:10.1007/s10515-014-0154-2
[32] Schrammel, P. (2013). Logico-numerical verification methods for discrete and hybrid systems. Ph.D. thesis, University of Grenoble.
[33] Smith, J.O. (2011). Spectral Audio Signal Processing. http://ccrma.stanford.edu/ jos/sasp/. Online book, 2011 edition.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.