Testing Stochastic Systems Using MoVoS Tool: Case Studies

  • Kenza Bouaroudj
  • Djamel-Eddine Saidouni
  • Ilham Kitouni
Part of the Communications in Computer and Information Science book series (CCIS, volume 403)


MoVoS tool is an implementation of testing theory based on stochastic refusals graph. It allows the automatic extraction of test cases from specification of stochastic systems. Those systems are modeled by Maximality based Labeled Stochastic Transition System “MLSTS”.

In This paper, we present the application of MoVoS tool on two cases studies to valid it. Those case studies permit us to illustrate the functionality of tool and to show that this tool can deal with large system.


formal testing models refusals graphs maximality semantics canonical tester 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Arous, M., Saidouni, D.E., Ilié, J.M.: Maximality Semantics based Stochastic Process Algebra for Performance Evaluation. In: 1st IEEE International Conference on Communications, Computing and Control Applications (CCCA 2011), Hammamet, Tunisia, March 3-5 (2011), IEEE Catalog Number: CFP1154M-ART, ISBN: 978-1-4244-9796-6Google Scholar
  2. 2.
    Arous, M., Saidouni, D.E., Ilié, J.M.: Addressing State Space Explosion Problem in Performance Evaluation Using Maximality-based Labeled Stochastic Transition Systems. In: to appear in 2nd International Conference on Computer and Software Modeling - ICCSM 2012, Cochin, India, October 20-21. IPCSIT (2012)Google Scholar
  3. 3.
    Arous, M., Bouaroudj, K., Saïdouni, D.E.: An environment for modeling and verifying / testing stochastic systems. Issues of JATIT 50 ( appear in April 2013)Google Scholar
  4. 4.
    Belinfante, A., Feenstra, J., de Vries, R.G., Tretmans, J., Goga, N., Feijs, L., Mauw, S., Heerink, L.: Formal test automation: A simple experiment. In: 12th Int. Workshop on Testing of Communicating Systems. Kluwer (1999)Google Scholar
  5. 5.
    Bouaroudj, K., Kitouni, I., Hachichi, H., Saidouni, D.E.: Extending Refusal Testing by Stochastic Refusals for Testing Non-deterministic Systems. IJCSI 9(5) (September 2012)Google Scholar
  6. 6.
    Brinksma, E.: A theory for the derivation of tests. In: Aggarwal, S., Sabnani, K. (eds.) Proceedings of the 8th IFIP Symposium on Protocol Specification, Testing and Verification (PSTV 1988). North-Holland (1989)Google Scholar
  7. 7.
    Tschaen, V.: 6 test generation algorithms based on preorder relations. In: Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.) Model-Based Testing of Reactive Systems. LNCS, vol. 3472, pp. 151–171. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  8. 8.
    Burns, A.: How to verify a safe real time: the application of model checking and timed automata to the production cell case study. Real Time Systems Journal 24(2), 135–152 (2003)CrossRefzbMATHGoogle Scholar
  9. 9.
    Clarke, D., Jéron, T., Rusu, V., Zinovieva, E.: STG: A symbolic test generation tool. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 470–475. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  10. 10.
    Jalali, V., Borujerdi, M.R.M.: A hybrid information retrieval system for medical field using meSH ontology. In: Prasad, S.K., Routray, S., Khurana, R., Sahni, S. (eds.) ICISTM 2009. CCIS, vol. 31, pp. 31–40. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  11. 11.
    Hessel, A., Larsen, K.G., Nielsen, B., Pettersson, P., Skou, A.: Time-optimal real-time test case generation using uppaal. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 114–130. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  12. 12.
    Holton, D.R.W.: A PEPA Specification of an Industrial Production Cell. The Computer Journal 38(7), 542–551 (1995)CrossRefGoogle Scholar
  13. 13.
    Jard, C., Jéron., T.: Tgv: theory, principles and algorithms, a tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems. Software Tools for Technology Transfer (STTT) 10 (2004)Google Scholar
  14. 14.
    Nielsen, B., Skou, A.: Automated test generation from timed automata. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 343–357. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  15. 15.
    Nielsen, B.: Specification and test of real-time systems: PhD thesis, Aalborg University (April 2000)Google Scholar
  16. 16.
    Saïdouni, D.E., Courtiat, J.P.: Prise en compte des durées d’action dans les algèbres de processus par l’utilisation de la sémantique de maximalité. In: Proceedings of CFIP 2003, Hermes, France (2003)Google Scholar
  17. 17.
    Tyszberowiez, S.S.: How to implement a safe real-time system: The OBSERV implementation of the production cell case study. Real Time Systems 15(1), 61–90 (1998)CrossRefGoogle Scholar
  18. 18.
    Kamrul, H.T.: Formal verification of the Alternating Bit Protocol. In: 6th International Conference on Computer & Information Technology, ICCIT (2003)Google Scholar
  19. 19.
    Groote, J.F., Springintveld, J.: Focus points and convergent process perators. A proof strategy for protocol verification. Journal of Logic and Algebraic Programming 49(1/2), 31–60 (2001)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Kenza Bouaroudj
    • 1
  • Djamel-Eddine Saidouni
    • 1
  • Ilham Kitouni
    • 1
  1. 1.MISC LaboratoryUniversity Constantine 2Algeria

Personalised recommendations