Extended Institutions for Testing

  • Marielle Doche
  • Virginie Wiels
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1816)


In this paper, we present an extension of the notion of institution that takes into account test cases. Our approach is to incrementally generate functional tests from a structured formal specification, we generate tests from small specifications and compose them. The issue is then to prove the correctness of the resulting tests. We thus extend the classical notion of institution with a category of test cases and a notion of satisfaction of test cases.


Functional test generation formal specification category theory institutions 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Arrais and J. L. Fiadeiro. Unifying theories in different institutions. In Recent Trends in Data Type Specification, volume 1130 of LNCS, pages 81–101. Springer Verlag, 1996.Google Scholar
  2. 2.
    S. Barbey, D. Buchs, and C. Péraire. Test selection for object-oriented software based on formal specifications. In Proceedings of PROCOMET’98, number Technical Report EPFL-DI No 97/252, December 1997.Google Scholar
  3. 3.
    G. Bernot, M-C. Gaudel, and B. Marre. Software testing based on formal specifications: a theory and a tool. Software Engineering Journal, 6, November 1991.Google Scholar
  4. 4.
    E. Brinksma. Formal methods for conformance testing: Theory can be practical. In CAV’99, number 1633 in LNCS, pages 44–46. Springer Verlag, July 1999.Google Scholar
  5. 5.
    J. Cazin, C. Seguin, W. Osnowycz, E. Ciapessoni, and E. Ratto. An experience in the specification and test of an electrical flight control system using a temporal logic framework. InDASIA 96 Data Systems in Aerospace. ESA publications, May 1996.Google Scholar
  6. 6.
    E. Ciapessoni, E. Corsetti, M. Migliorati, and E. Ratto. Specifying industrial real-time systems in a logical framework. In ICLP 94-Post Conference Workshop on Logic Programming in Software Engineering, 1994.Google Scholar
  7. 7.
    A. Daurat, M. Doche, and D. Le Berre. Manipulations des principaux objets du formalisme Moka-TRIO par l’interface Java-Moka. ONERA-CERT / DTIM, 1999.Google Scholar
  8. 8.
    M. Doche. Techniques formelles pour l’évaluation de systèmes complexes. Test et modularité. PhD thesis, ENSAE, ONERA-CERT/DTIM, December 1999.Google Scholar
  9. 9.
    M. Doche, C. Seguin, and V. Wiels. A modular approach to specify and test an electrical flight control system. In FMICS-4, Fourth International Workshop on Formal Methods for Industrial Critical Systems, July 1999.Google Scholar
  10. 10.
    H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 2: Modules specifications and constraints, volume 21 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1990.Google Scholar
  11. 11.
    J. Fiadeiro and T. Maibaum. Temporal theories as modularisation units for concurrent system specification. Formal Aspects of Computing, 4(3):239–272, 1992.zbMATHCrossRefGoogle Scholar
  12. 12.
    J.H. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper and Row, 1986.Google Scholar
  13. 13.
    M-C. Gaudel. Testing can be formal, too. In TAPSOFT’95, pages 82–96. Springer Verlag, 1995.Google Scholar
  14. 14.
    C. Ghezzi, D. Mandrioli, and A. Morzenti. A model parametric real-time logic. ACM Transactions on programming languages and systems, 14(4):521–573, October 1992.CrossRefGoogle Scholar
  15. 15.
    J. A. Goguen and R. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the ACM, 39(1):95–146, January 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    T. Jéron and P. Morel. Test generation derived from model-checking. In Computer Aided Verification, CAV’99, volume 1633 of LNCS, pages 108–121. Springer-Verlag, July 1999.CrossRefGoogle Scholar
  17. 17.
    D. Mandrioli, S. Morasca, and A. Morzenti. Functionnal test case generation for real-time systems. In Dependable computing for critical applications 3., volume 8 of Dependable computing and fault-tolerant systems, pages 29–61. Springer Verlag, 1992.Google Scholar
  18. 18.
    J. Meseguer. General logics. In H-D. Ebbinghaus and all, editors, Proceedings of Logic Colloquium. North-Holland, 1987.Google Scholar
  19. 19.
    P. Michel and V. Wiels. A framework for modular formal specification and verification. In Proceedings of FME’97, number 1313 in LNCS. Springer-Verlag, 1997.Google Scholar
  20. 20.
    C. Seguin and W. Wiels. Using a logical and categorical approach for the validation of fault-tolerant systems. In FME96, Formal Methods Europe, March 1996.Google Scholar
  21. 21.
    V. Wiels. Modularité pour la conception et la validation formelles de systèmes. PhD thesis, ENSAE-ONERA/CERT/DERI, October 1997.Google Scholar
  22. 22.
    V. Wiels and S. Easterbrook. Management of evolving specifications using category theory. In Proceedings of Automated Software Engineering’98, 1998.Google Scholar
  23. 23.
    M. Wirsing. Algebraic specification. In Handbook of theoretical computer science, Formal Models and Semantics, volume B, pages 675–788. Elsevier and MIT Press, 1990.MathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Marielle Doche
    • 1
  • Virginie Wiels
    • 2
  1. 1.Department of Electronics and Computer ScienceUniversity of SouthamptonHighfield SouthamptonUK
  2. 2.ONERA-CERT/DTIMToulouse Cedex 4France

Personalised recommendations