Abstract
Testing remains a widely used validation technique for software systems. However, recent needs in software development (e.g., in terms of security concerns) may require to extend this technique to address a larger set of properties. In this article, 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 w.r.t. several relations of interest. For each relation, we give a sufficient condition for a property to be testable. Then, we study and delineate a fine-grain characterization of testable properties: for each Safety-Progress class, we identify the subset of testable properties and their corresponding test oracle. Furthermore, we address automatic test generation for the proposed framework by providing a general synthesis technique that allows to obtain canonical testers for the testable properties in the Safety-Progress classification. Moreover, we show how the usual notion of quiescence can be taken into account in our general framework, and, how quiescence improves the testability results. Then, we list some existing testing approaches that could benefit from this work by addressing a wider set of properties. Finally, we propose Java-PT, a prototype Java toolbox that implements the results introduced in this article.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Alpern B., Schneider F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181–185 (1985)
Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Logic Comput. 20(3) (2010)
Cerná, I., Pelánek, R.: Relating the hierarchy of temporal properties to model checking. In: MFCS 2003: Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 2747, pp. 318–327. Springer (2003)
Chang, E., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 623, pp. 474–486. Springer (1992)
Chang, E., Manna, Z., Pnueli, A.: The safety-progress classification. Technical report, Stanford University, Department of Computer Science (1992)
Constant C., Jéron T., Marchand H., Rusu V.: Integrating formal verification and conformance testing for reactive systems. IEEE Trans. Softw. Eng. 33(8), 558–574 (2007)
Darmaillacq V., Fernandez J.-C., Groz R., Mounier L., Richier J.-L.: Test generation for network security rules. In: Ümit Uyar, M., Duale, A.Y., Fecko, M.A. (eds) TestCom. Lecture Notes in Computer Science, vol. 3964, pp. 341–356. Springer, Berlin (2006)
Darmaillacq, V., Richier, J.-L., Groz, R.: Test generation and execution for security rules in temporal logic. In: ICSTW ’08: Proceedings of the 2008 IEEE International Conference on Software Testing Verification and Validation Workshop, pp. 252–259. IEEE Computer Society (2008)
de Vries, R.G.: Towards formal test purposes. In: Tretmans, J., Brinksma, Ed. (eds.) FATES’01: Formal Approaches to Testing of Software. BRICS Notes Series, pp. 61–76 (2001)
Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science. Formal Models and Sematics (B), vol. B, pp. 995–1072. MIT Press (1990)
Falcone Y., Fernandez J.-C., Jéron T., Marchand H., Mounier L.: More testable properties. In: Petrenko, A., da Silva Simão, A., Maldonado, J.C. (eds) ICTSS. Lecture Notes in Computer Science, vol. 6435, pp. 30–46. Springer, Berlin (2010)
Falcone, Y., Fernandez, J.-C., Mounier, L.: Runtime verification of safety-progress properties. In: The 9th Int. Workshop on Runtime Verification. Lecture Notes in Computer Science, vol. 5779, pp. 40–59. Springer (2009)
Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? Softw. Tools Technol. Transfer (2011). doi:10.1007/s10009-011-0196-8
Falcone Y., Fernandez J.-C., Mounier L., Richier J.-L.: A test calculus framework applied to network security policies. In: Havelund, K., Núñez, M., Rosu, G., Wolff, B. (eds) FATES/RV. Lecture Notes in Computer Science, vol. 4262, pp. 55–69. Springer, Berlin (2006)
Falcone, Y., Fernandez, J.-C., Mounier, L., Richier, J.-L.: A compositional testing framework driven by partial specifications. In: TestCom/FATES. Lecture Notes in Computer Science, vol. 4581, pp. 107–122. Springer (2007)
Fernandez J.-C., Mounier L., Pachon C.: Property oriented test case generation. In: Petrenko, A., Ulrich, A. (eds) FATES. Lecture Notes in Computer Science, vol. 2931, pp. 147–163. Springer, Berlin (2003)
Grabowski, Jens: SDL and MSC based test case generation—an overall view of the SAMSTAG method. Technical report, University of Berne, IAM-94-0005 (1994)
Jard C., Jéron T.: TGV: theory, principles and algorithms. Softw. Tools Technol. Transfer 7(4), 297–315 (2005)
Koch, B., Grabowski, J., Hogrefe, D., Schmitt, M. II: Autolink: a tool for automatic test generation from SDL specifications. In: WIFT, p. 114. IEEE Computer Society (1998)
Lamport L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125–143 (1977)
Machado, P.D.L., Silva, D.A., Mota, A.C.: Towards property oriented testing. In: Proceedings of the Second Brazilian Symposium on Formal Methods (SBMF 2005). Electron. Notes Theor. Comput. Sci., vol. 184, pp. 3–19. Elsevier, Amsterdam (2007)
Mallouli, W., Orset, J.-M., Cavalli, A., Cuppens, N., Cuppens, F.: A formal approach for testing security rules. In: SACMAT ’07: Proceedings of the 12th ACM symposium on Access Control Models and Technologies, pp. 127–132. ACM, New York (2007)
Manna, Z., Pnueli, A.: A hierarchy of temporal properties (invited paper, 1989). In: PODC’90: Proceedings of the 9th Symposium on Principles of Distributed Computing, pp. 377–410. ACM, New York (1990)
Marchand, H., Dubreil, J., Jéron, T.: Automatic testing of access control for security properties. In: TestCom/FATES’09. Lecture Notes in Computer Science, vol. 5826, pp. 113–128. Springer, Berlin (2009)
Nahm, R., Grabowski, J., Hogrefe, D.: Test case generation for temporal properties. Technical report, Bern University (1993)
Pecheur, C., Raimondi, F., Brat, G.: A formal analysis of requirements-based testing. In: ISSTA’09: Proceedings of the 18th International Symposium on Software Testing and Analysis, pp. 47–56. ACM, New York (2009)
Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: FM06: Proceedings of the 14th Int. Symp. on Formal Methods. Lecture Notes in Computer Science, vol. 4085, pp. 573–586. Springer, New York (2006)
Rajan, A., Whalen, M.W., Heimdahl, M.R.: Model validation using automatically generated requirements-based tests. In: HASE ’07: 10th IEEE Symposium on High Assurance Systems Engineering, pp. 95–104. IEEE Computer Society (2007)
Streett, R.S.: Propositional dynamic logic of looping and converse. In: STOC ’81: Proceedings of the 13th Symp. on Theory of Computing, pp. 375–383. ACM, New York (1981)
Traon, Y.L., Mouelhi, T., Baudry, B.: Testing security policies: going beyond functional testing. In: 18th IEEE Int. Symp. on Software Reliability Engineering, pp. 93–102, Los Alamitos, CA, USA. IEEE Computer Society (2007)
Tretmans, J.: A formal approach to conformance testing. In: Rafiq, O. (ed.) Protocol Test Systems. IFIP Transactions, vol. C-19, pp. 257–276. North-Holland (1993)
Tretmans J.: Test generation with inputs, outputs, and quiescence. In: Margaria, T., Steffen, B. (eds) TACAS. Lecture Notes in Computer Science, vol. 1055, pp. 127–146. Springer, Berlin (1996)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Falcone, Y., Fernandez, JC., Jéron, T. et al. More testable properties. Int J Softw Tools Technol Transfer 14, 407–437 (2012). https://doi.org/10.1007/s10009-011-0220-z
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-011-0220-z