Abstract
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.
An extended version of this paper with complete proofs can be found in [1].
Chapter PDF
References
Falcone, Y., Fernandez, J.C., Jéron, T., Marchand, H., Mounier, L.: More Testable Properties. Technical Report 7279, INRIA (2010)
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)
Jard, C., Jéron, T.: TGV: theory, principles and algorithms. International Journal on Software Tools for Technology Transfer (STTT), 297–315 (2005)
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)
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)
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)
Nahm, R., Grabowski, J., Hogrefe, D.: Test Case Generation for Temporal Properties. Technical report, Bern University (1993)
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)
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)
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)
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)
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)
Lamport, L.: Proving the Correctness of Multiprocess Programs. IEEE Trans. Softw. Eng., 125–143 (1977)
Alpern, B., Schneider, F.B.: Defining Liveness. Technical report, Cornell University, Ithaca, NY, USA (1984)
Chang, E., Manna, Z., Pnueli, A.: The Safety-Progress Classification. Technical report, Stanford University, Dept. of Computer Science (1992)
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)
Falcone, Y., Fernandez, J.C., Mounier, L.: What can You Verify and Enforce at Runtime? Technical Report TR-2010-5, Verimag Research Report (2010)
Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL Semantics for Runtime Verification. Journal of Logic and Computation (2009)
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)
de Vries, R.G.: Towards formal test purposes. In: FATES 2001: Formal Approaches to Testing of Software, pp. 61–76 (2001)
Machado, P.D.L., Silva, D.A., Mota, A.C.: Towards Property Oriented Testing. Electron. Notes Theor. Comput. Sci., 3–19 (2007)
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)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 IFIP International Federation for Information Processing
About this paper
Cite this paper
Falcone, Y., Fernandez, JC., Jéron, T., Marchand, H., Mounier, L. (2010). More Testable Properties. In: Petrenko, A., Simão, A., Maldonado, J.C. (eds) Testing Software and Systems. ICTSS 2010. Lecture Notes in Computer Science, vol 6435. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16573-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-16573-3_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16572-6
Online ISBN: 978-3-642-16573-3
eBook Packages: Computer ScienceComputer Science (R0)