Test generation from P systems using model checking

Article English OPEN
Ipate, Florentin ; Gheorghe, Marian ; Lefticaru, Raluca (2010)
  • Publisher: Elsevier BV
  • Journal: The Journal of Logic and Algebraic Programming, volume 79, issue 6, pages 350-362 (issn: 1567-8326)
  • Related identifiers: doi: 10.1016/j.jlap.2010.03.007
  • Subject: Theoretical Computer Science | Computational Theory and Mathematics | Software | Logic

This paper presents some testing approaches based on model checking and using different testing criteria. First, test sets are built from different Kripke structure representations. Second, various rule coverage criteria for transitional, non-deterministic, cell-like P systems, are considered in order to generate adequate test sets. Rule based coverage criteria (simple rule coverage, context-dependent rule coverage and variants) are defined and, for each criterion, a set of LTL (Linear Temporal Logic) formulas is provided. A codification of a P system as a Kripke structure and the sets of LTL properties are used in test generation: for each criterion, test cases are obtained from the counterexamples of the associated LTL formulas, which are automatically generated from the Kripke structure codification of the P system. The method is illustrated with an implementation using a specific model checker, NuSMV. (C) 2010 Elsevier Inc. All rights reserved.
  • References (26)
    26 references, page 1 of 3

    [1] P.E. Ammann, P.E. Black, W. Majurski, Using model checking to generate tests from specifications, in: Proceedings of the Second IEEE International Conference on Formal Engineering Methods, ICFEM '98, IEEE Computer Society, 1998, p. 46.

    [2] A. Cimatti, E.M. Clarke, F. Giunchiglia, M. Roveri, NuSMV: A new symbolic model checker, International Journal on Software Tools for Technology Transfer 2 (2000) 410-425.

    [3] G. Ciobanu, M.J. Pe´rez-Jime´nez, G. Pa˘un (Eds.), Applications of Membrane Computing, Natural Computing Series, Springer, 2006.

    [4] E.M. Clarke, E.A. Emerson, Design and synthesis of synchronization skeletons using branching-time temporal logic, 1981, in: D. Kozen (Ed.), Logic of Programs, Workshop, volume 131 of Lecture Notes in Computer Science, Springer, 1982, pp. 52-71.

    [5] E.M. Clarke, Jr., O. Grumberg, D.A. Peled, Model checking, MIT Press, Cambridge, MA, USA, 1999.

    [6] Z. Dang, O.H. Ibarra, C. Li, G. Xie, On the decidability of model-checking for P systems, Journal of Automata, Languages and Combinatorics 11 (2006) 279-298.

    [7] D. D´ıaz-Pernil, I. Pe´rez-Hurtado, M.J. Pe´rez-Jime´nez, A. Riscos-Nu´n˜ez, A P-lingua programming environment for membrane computing, in: D.W. Corne, P. Frisco, G. Pa˘un, G. Rozenberg, A. Salomaa (Eds.), Membrane Computing - 9th International Workshop, WMC 2008, Revised Selected and Invited Papers, volume 5391 of Lecture Notes in Computer Science, Springer, 2009, pp. 187-203.

    [8] E.A. Emerson, J.Y. Halpern, Decision procedures and expressiveness in the temporal logic of branching time, in: Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC '82, ACM, 1982, pp. 169-180.

    [9] A. Engels, L.M.G. Feijs, S. Mauw, Test generation for intelligent networks using model checking, in: E. Brinksma (Ed.), Tools and Algorithms for Construction and Analysis of Systems, Third International Workshop, TACAS '97, volume 1217 of Lecture Notes in Computer Science, Springer, 1997, pp. 384-398.

    [10] G. Fraser, F. Wotawa, P. Ammann, Testing with model checkers: a survey, Software Testing, Verification and Reliability 19 (2009) 215-261.

  • Metrics
    No metrics available
Share - Bookmark