Abstract
This talk reviews some of my contributions on formal testing of timed and probabilistic systems, focusing on methodologies that allow their users to decide whether these systems are correct with respect to a formal specification. The consideration of time and probability complicates the definition of these frameworks since there is not an obvious way to define correctness. For example, in a specific situation it might be desirable that a system is as fast as possible while in a different application it might be required that the performance of the system is exactly equal to the one given by the specification. All the methodologies have as common assumption that the system under test is a black-box and that the specification is described as a timed and/or probabilistic extension of the finite state machines formalism.
This research has been partially supported by the Spanish MICINN project TESIS (TIN2009-14312-C02-01) and by the Santander-UCM Programme to fund research groups (GR35/10-A-910606).
Chapter PDF
References
Andrés, C., Maag, S., Cavalli, A., Merayo, M., Núñez, M.: Analysis of the OLSR protocol by using formal passive testing. In: 16th Asia-Pacific Software Engineering Conference, APSEC 2009, pp. 152–159. IEEE Computer Society, Los Alamitos (2009)
Andrés, C., Merayo, M., Núñez, M.: Applying formal passive testing to study temporal properties of the stream control transmission protocol. In: 7th IEEE Int. Conf. on Software Engineering and Formal Methods, SEFM 2009, pp. 73–82. IEEE Computer Society, Los Alamitos (2009)
Andrés, C., Merayo, M., Núñez, M.: Formal passive testing of timed systems: Theory and tools. Software Testing, Verification and Reliability (2012) (accepted for publication)
Derderian, K., Merayo, M., Hierons, R., Núñez, M.: Aiding test case generation in temporally constrained state based systems using genetic algorithms. In: Cabestany, J., Sandoval, F., Prieto, A., Corchado, J.M. (eds.) IWANN 2009. LNCS, vol. 5517, pp. 327–334. Springer, Heidelberg (2009)
Derderian, K., Merayo, M., Hierons, R., Núñez, M.: A case study on the use of genetic algorithms to generate test cases for temporal systems. In: Cabestany, J., Rojas, I., Joya, G. (eds.) IWANN 2011, Part II. LNCS, vol. 6692, pp. 396–403. Springer, Heidelberg (2011)
Gaudel, M.C.: Testing can be formal, too! In: Mosses, P.D., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol. 915, pp. 82–96. Springer, Heidelberg (1995)
Glabbeek, R.v., Smolka, S., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Information and Computation 121(1), 59–80 (1995)
Hennessy, M.: Algebraic Theory of Processes. MIT Press, Cambridge (1988)
Hierons, R., Bogdanov, K., Bowen, J., Cleaveland, R., Derrick, J., Dick, J., Gheorghe, M., Harman, M., Kapoor, K., Krause, P., Luettgen, G., Simons, A., Vilkomir, S., Woodward, M., Zedan, H.: Using formal methods to support testing. ACM Computing Surveys 41(2) (2009)
Hierons, R., Núñez, M.: Testing probabilistic distributed systems. In: Hatcliff, J., Zucca, E. (eds.) FMOODS 2010. LNCS, vol. 6117, pp. 63–77. Springer, Heidelberg (2010)
Llana, L., Núñez, M.: Testing semantics for RTPA. Fundamenta Informaticae 90(3), 305–335 (2009)
López, N., Núñez, M., Rodríguez, I.: Specification, testing and implementation relations for symbolic-probabilistic systems. Theoretical Computer Science 353(1-3), 228–248 (2006)
Merayo, M., Hwang, I., Núñez, M., Cavalli, A.: A statistical approach to test stochastic and probabilistic systems. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 186–205. Springer, Heidelberg (2009)
Merayo, M., Núñez, M., Hierons, R.: Testing timed systems modeled by stream X-machines. Software and Systems Modeling 10(2), 201–217 (2011)
Merayo, M., Núñez, M., Rodríguez, I.: Extending EFSMs to specify and test timed systems with action durations and timeouts. IEEE Transactions on Computers 57(6), 835–848 (2008)
Merayo, M., Núñez, M., Rodríguez, I.: Formal testing from timed finite state machines. Computer Networks 52(2), 432–460 (2008)
Merayo, M., Núñez, M., Rodríguez, I.: A formal framework to test soft and hard deadlines in timed systems. Software Testing, Verification and Reliability (accepted for publication, 2011), doi: 10.1002/stvr.448
de Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoretical Computer Science 34, 83–133 (1984)
Núñez, M.: Algebraic theory of probabilistic processes. Journal of Logic and Algebraic Programming 56(1-2), 117–177 (2003)
Núñez, M., Llana, L.: A hierarchy of equivalences for probabilistic processes. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol. 5048, pp. 267–282. Springer, Heidelberg (2008)
Sidhu, D., Leung, T.K.: Formal methods for protocol testing: A detailed study. IEEE Transactions on Software Engineering 15(4), 413–426 (1989)
Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 1–38. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 IFIP International Federation for Information Processing
About this paper
Cite this paper
Núñez, M. (2011). Formal Testing of Timed and Probabilistic Systems. In: Wolff, B., Zaïdi, F. (eds) Testing Software and Systems. ICTSS 2011. Lecture Notes in Computer Science, vol 7019. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24580-0_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-24580-0_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24579-4
Online ISBN: 978-3-642-24580-0
eBook Packages: Computer ScienceComputer Science (R0)