LOGIN TO YOUR ACCOUNT

Username
Password
Remember Me
Or use your Academic/Social account:

CREATE AN ACCOUNT

Or use your Academic/Social account:

Congratulations!

You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.

Important!

Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message

CREATE AN ACCOUNT

Name:
Username:
Password:
Verify Password:
E-mail:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Ipate, Florentin; Gheorghe, Marian; Lefticaru, Raluca (2010)
Publisher: Elsevier BV
Journal: The Journal of Logic and Algebraic Programming
Languages: English
Types: Article
Subjects: Theoretical Computer Science, Computational Theory and Mathematics, Software, Logic

Classified by OpenAIRE into

ACM Ref: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
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.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • [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.
    • [11] M. Garc´ıa-Quismondo, R. Gutie´rrez-Escudero, I. Pe´rez-Hurtado, M.J. Pe´rez-Jime´nez, A. Riscos-Nu´n˜ez, An overview of P-Lingua 2.0, in: G. Pa˘un, M.J. Pe´rez-Jime´nez, A. Riscos-Nu´n˜ez, G. Rozenberg, A. Salomaa (Eds.), Membrane Computing - 10th International Workshop, WMC 2009, Revised Selected and Invited Papers, volume 5957 of Lecture Notes in Computer Science, Springer, 2010, pp. 264-288.
    • [12] A. Gargantini, C.L. Heitmeyer, Using model checking to generate tests from requirements specifications, in: O. Nierstrasz, M. Lemoine (Eds.), Software Engineering - ESEC/FSE'99, 7th European Software Engineering Conference, volume 1687 of Lecture Notes in Computer Science, Springer, 1999, pp. 146-162.
    • [13] M. Gheorghe, F. Ipate, On testing P systems, 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. 204-216.
    • [14] R. Hierons, K. Bogdanov, J. Bowen, R. Cleaveland, J. Derrick, J. Dick, M. Gheorghe, M. Harman, K. Kapour, P. Krause, G. Luettgen, A. Simons, S. Vilkomir, M. Woodward, H. Zedan, Using formal specifications to support testing, ACM Compt. Surv. 41 (2009).
    • [15] M. Holcombe, F. Ipate, Correct Systems: Building a Business Process Solution, Applied Computing Series, Springer-Verlag, Berlin, Germany, 1998.
    • [16] H.S. Hong, I. Lee, O. Sokolsky, S.D. Cha, Automatic test generation from statecharts using model checking, in: In Proceedings of FATES'01, Workshop on Formal Approaches to Testing of Software, volume NS-01-4 of BRICS Notes Series, pp. 15-30.
    • [17] H.S. Hong, I. Lee, O. Sokolsky, H. Ural, A temporal logic based theory of test coverage and generation, in: J.P. Katoen, P. Stevens (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, volume 2280 of Lecture Notes in Computer Science, Springer, 2002, pp. 327-341.
    • [18] F. Ipate, M. Gheorghe, Finite state based testing of P systems, Natural Computing 8 (2009) 833-846.
    • [19] F. Ipate, M. Gheorghe, Mutation based testing of P systems, International Journal of Computers, Communications & Control 4 (2009) 253-262.
    • [20] F. Ipate, M. Gheorghe, Testing non-deterministic stream x-machine models and p systems, Electronic Notes in Theoretical Computer Science 227 (2009) 113-126.
    • [21] K.L. McMillan, Symbolic Model Checking, Kluwer Academic Publ., 1993.
    • [22] A. Pnueli, The temporal logic of programs, in: 18th Annual Symposium on Foundations of Computer Science, IEEE, 1977, pp. 46-57.
    • [23] A. Pnueli, The temporal semantics of concurrent programs, Theoretical Computer Science 13 (1981) 45-60.
    • [24] G. Pa˘un, Computing with membranes, Journal of Computer and System Sciences 61 (2000) 108-143.
    • [25] G. Pa˘un, Membrane Computing: An Introduction, Springer-Verlag, 2002.
    • [26] G. Pa˘un, G. Rozenberg, A. Salomaa (Eds.), The Oxford Handbook of Membrane Computing, Oxford University Press, 2010.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article