A constraint solver for sequences and its applications

ABSTRACT

Constraint programming techniques are successfully used in various areas of software engineering for industry, commerce, transport, finance etc. Constraint solvers for different data types are applied in validation and verification of programs containing data elements of these types. A general constraint solver for sequences is necessary to take into account this data type in the existing validation and verification tools. In this work, we present an original constraint solver for sequences implemented in CHR and based on T. Frühwirth's solver for lists with the propagation of two constraints: generalized concatenation and size. The applications of the solver (with the validation and verification tool BZTT) to different software engineering problems are illustrated by the example of a waiting room model.

REFERENCES

• 1: J.-R. Abrial, The B-book: assigning programs to meanings, Cambridge University Press, New York, NY, 1996
• 2: M. Lothaire. Algebraic Combinatorics on Words. Cambridge University Press, 2002. ISBN 0521812208.
• 3: L. Berkaoui, B. Legeard. Représentation de séquences définies sur des ensembles non instanciés par arbre PQR partiel. In Actes de JFPLC'98, Nantes, France, 251--266, May 1998. Hermès.
• 4: Fabrice Bouquet , Bruno Legeard , Fabien Peureux, CLPS–B – A constraint solver to animate a B specification, International Journal on Software Tools for Technology Transfer (STTT), v.6 n.2, p.143-157, August 2004 [doi>10.1007/s10009-003-0123-8]
• 5: The BZ-Testing-Tools web site, http://lifc.univ-fcomte.fr/~bztt, Université de Franche-Comté, Besançon.
• 6: Alain Colmerauer, An introduction to Prolog III, Communications of the ACM, v.33 n.7, p.69-90, July 1990 [doi>10.1145/79204.79210]
• 7: Valery Durnev, Studying Algorithmic Problems for Free Semi-groups and Groups, Proceedings of the 4th International Symposium on Logical Foundations of Computer Science, p.88-101, July 06-12, 1997
• 8: T. Frühwirth. Theory and Practice of Constraint Handling Rules. In: P. Stuckey, K. Marriot (Eds.). Special Issue on Constraint Logic Programming. Journal of Logic Programming, 37(1998), No. 1--3, 95--138.
• 9: T. Frühwirth. The CHR web site. http://www.informatik.uni-ulm.de/pm/fileadmin/pm/home/fruehwirth/chr.html, Universität Ulm.
• 10: Juhani Karhumäki , Filippo Mignosi , Wojciech Plandowski, The expressibility of languages and relations by word equations, Journal of the ACM (JACM), v.47 n.3, p.483-505, May 2000 [doi>10.1145/337244.337255]
• 11: Antoni Kościelski , Leszek Pacholski, Complexity of Makanin's algorithm, Journal of the ACM (JACM), v.43 n.4, p.670-684, July 1996 [doi>10.1145/234533.234543]
• 12: N. Kosmatov. Constraint solving for sequences web site. http://lifc.univ-fcomte.fr/~kosmatov/sequences, Université de Franche-Comté, Besançon.
• 13: Nikolai Kosmatov , Bruno Legeard , Fabien Peureux , Mark Utting, Boundary Coverage Criteria for Test Generation from Formal Models, Proceedings of the 15th International Symposium on Software Reliability Engineering (ISSRE'04), p.139-150, November 02-05, 2004 [doi>10.1109/ISSRE.2004.12]
• 14: G. S. Makanin. The problem of solvability of equations in a free semigroup. Mat. Sbornik (N.S.), 103 (1977), No. 2, 147--236 (in Russian). English translation in: Math. URSS Sbornik, 32(1977), 129--198.
• 15: J. M. Spivey, The Z notation: a reference manual, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1992

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Algorithms, Verification

Keywords:
constraint solver, sequences, validation, verification