Journal
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING
Volume 79, Issue 6, Pages 350-362Publisher
ELSEVIER SCIENCE INC
DOI: 10.1016/j.jlap.2010.03.007
Keywords
P systems; Kripke structures; Model checking; Test generation
Categories
-
Funding
- CNCSIS - UEFISCSU [PNII - IDEI 643/2008]
Ask authors/readers for more resources
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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available