More Testable Properties

  • Yliès Falcone
  • Jean-Claude Fernandez
  • Thierry Jéron
  • Hervé Marchand
  • Laurent Mounier
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6435)


In this paper, we explore the set of testable properties within the Safety-Progress classification where testability means to establish by testing that a relation, between the tested system and the property under scrutiny, holds. We characterize testable properties wrt. several relations of interest. For each relation, we give a sufficient condition for a property to be testable. Then, we study and delineate, for each Safety-Progress class, the subset of testable properties and their corresponding test oracle producing verdicts for the possible test executions. Finally, we address automatic test generation for the proposed framework.


Test Generation Testable Property Execution Sequence Test Case Generation Interaction Sequence 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Falcone, Y., Fernandez, J.C., Jéron, T., Marchand, H., Mounier, L.: More Testable Properties. Technical Report 7279, INRIA (2010)Google Scholar
  2. 2.
    Koch, B., Grabowski, J., Hogrefe, D., Schmitt, M.: Autolink: A Tool for Automatic Test Generation from SDL Specifications. In: Industrial-Strength Formal Specification Techniques (1998)Google Scholar
  3. 3.
    Jard, C., Jéron, T.: TGV: theory, principles and algorithms. International Journal on Software Tools for Technology Transfer (STTT), 297–315 (2005)Google Scholar
  4. 4.
    Traon, Y.L., Mouelhi, T., Baudry, B.: Testing Security Policies: Going Beyond Functional Testing. In: Int. Symp. on Software Reliability Engineering, pp. 93–102 (2007)Google Scholar
  5. 5.
    Mallouli, W., Orset, J.M., Cavalli, A., Cuppens, N., Cuppens, F.: A Formal Approach for Testing Security Rules. In: SACMAT 2007: Proceedings of the 12th ACM symposium on Access control models and technologies, pp. 127–132. ACM, New York (2007)CrossRefGoogle Scholar
  6. 6.
    Constant, C., Jéron, T., Marchand, H., Rusu, V.: Integrating Formal Verification and Conformance Testing for Reactive Systems. IEEE Trans. Software Eng. 33, 558–574 (2007)CrossRefGoogle Scholar
  7. 7.
    Nahm, R., Grabowski, J., Hogrefe, D.: Test Case Generation for Temporal Properties. Technical report, Bern University (1993)Google Scholar
  8. 8.
    Grabowski, J.: SDL and MSC based test case generation– an overall view of the SAMSTAG method. Technical report, University of Berne IAM-94-0005 (1994)Google Scholar
  9. 9.
    Chang, E., Manna, Z., Pnueli, A.: Characterization of Temporal Property Classes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 474–486. Springer, Heidelberg (1992)Google Scholar
  10. 10.
    Falcone, Y., Fernandez, J.C., Mounier, L.: Runtime Verification of Safety-Progress Properties. In: The 9th Int. Workshop on Runtime Verification, pp. 40–59 (2009)Google Scholar
  11. 11.
    Pnueli, A., Zaks, A.: PSL Model Checking and Run-Time Verification Via Testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Manna, Z., Pnueli, A.: A Hierarchy of Temporal Properties (invited paper 1989). In: PODC 1990: Proceedings of The 9th symp. on Principles Of Distributed Computing, pp. 377–410. ACM, New York (1990)CrossRefGoogle Scholar
  13. 13.
    Lamport, L.: Proving the Correctness of Multiprocess Programs. IEEE Trans. Softw. Eng., 125–143 (1977)Google Scholar
  14. 14.
    Alpern, B., Schneider, F.B.: Defining Liveness. Technical report, Cornell University, Ithaca, NY, USA (1984)Google Scholar
  15. 15.
    Chang, E., Manna, Z., Pnueli, A.: The Safety-Progress Classification. Technical report, Stanford University, Dept. of Computer Science (1992)Google Scholar
  16. 16.
    Streett, R.S.: Propositional Dynamic Logic of looping and converse. In: STOC 1981: Proceedings of the 13th Symp. on Theory Of computing, pp. 375–383. ACM, New York (1981)Google Scholar
  17. 17.
    Falcone, Y., Fernandez, J.C., Mounier, L.: What can You Verify and Enforce at Runtime? Technical Report TR-2010-5, Verimag Research Report (2010)Google Scholar
  18. 18.
    Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL Semantics for Runtime Verification. Journal of Logic and Computation (2009)Google Scholar
  19. 19.
    Tretmans, J.: Test Generation with Inputs, Outputs, and Quiescence. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. Tretmans, J, vol. 1055, pp. 127–146. Springer, Heidelberg (1996)Google Scholar
  20. 20.
    de Vries, R.G.: Towards formal test purposes. In: FATES 2001: Formal Approaches to Testing of Software, pp. 61–76 (2001)Google Scholar
  21. 21.
    Machado, P.D.L., Silva, D.A., Mota, A.C.: Towards Property Oriented Testing. Electron. Notes Theor. Comput. Sci., 3–19 (2007)Google Scholar
  22. 22.
    Rajan, A., Whalen, M., Heimdahl, M.: Model Validation using Automatically Generated Requirements-Based Tests. In: HASE 2007: 10th IEEE Symposium on High Assurance Systems Engineering, pp. 95–104 (November 2007)Google Scholar
  23. 23.
    Pecheur, C., Raimondi, F., Brat, G.: A Formal Analysis of Requirements-based Testing. In: ISSTA 2009: Proceedings of the 18th International Symposium on Software Testing and Analysis, pp. 47–56. ACM, New York (2009)Google Scholar
  24. 24.
    Darmaillacq, V., Fernandez, J.C., Groz, R., Mounier, L., Richier, J.L.: Test Generation for Network Security Rules. In: Uyar, M.Ü., Duale, A.Y., Fecko, M.A. (eds.) TestCom 2006. LNCS, vol. 3964, pp. 341–356. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  25. 25.
    Falcone, Y., Fernandez, J.C., Mounier, L., Richier, J.L.: A Compositional Testing Framework Driven by Partial Specifications. In: Petrenko, A., Veanes, M., Tretmans, J., Grieskamp, W. (eds.) TestCom/FATES 2007. LNCS, vol. 4581, pp. 107–122. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2010

Authors and Affiliations

  • Yliès Falcone
    • 1
  • Jean-Claude Fernandez
    • 2
  • Thierry Jéron
    • 1
  • Hervé Marchand
    • 1
  • Laurent Mounier
    • 2
  1. 1.INRIARennes - Bretagne AtlantiqueFrance
  2. 2.VERIMAGUniversité Grenoble IFrance

Personalised recommendations