| 11. |
- Beohar, Harsh, 1984-, et al.
(författare)
-
Basic behavioral models for software product lines : Expressiveness and testing pre-orders
- 2016
-
Ingår i: Science of Computer Programming. - Amsterdam : Elsevier. - 0167-6423 .- 1872-7964. ; 123, s. 42-60
-
Tidskriftsartikel (refereegranskat)abstract
- In order to provide a rigorous foundation for Software Product Lines (SPLs), several fundamental approaches have been proposed to their formal behavioral modeling. In this paper, we provide a structured overview of those formalisms based on labeled transition systems and compare their expressiveness in terms of the set of products they can specify. Moreover, we define the notion of tests for each of these formalisms and show that our notions of testing precisely capture product derivation, i.e., all valid products will pass the set of test cases of the product line and each invalid product fails at least one test case of the product line. © 2015 The Authors.
|
|
| 12. |
- Beohar, Harsh, 1984-, et al.
(författare)
-
Input–output conformance testing for software product lines
- 2016
-
Ingår i: The Journal of logical and algebraic methods in programming. - Amsterdam : Elsevier. - 2352-2208 .- 2352-2216. ; 85:6, s. 1131-1153
-
Tidskriftsartikel (refereegranskat)abstract
- We extend the theory of input-output conformance (IOCO) testing to accommodate behavioral models of software product lines (SPLs). We present the notions of residual and spinal testing. These notions allow for structuring the test process for SPLs by taking variability into account and extracting separate test suites for common and specific features of an SPL. The introduced notions of residual and spinal test suites allow for focusing on the newly introduced behavior and avoiding unnecessary re-test of the old one. Residual test suites are very conservative in that they require retesting the old behavior that can reach to new behavior. However, spinal test suites more aggressively prune the old tests and only focus on those test sequences that are necessary in reaching the new behavior. We show that residual testing is complete but does not usually lead to much reduction in the test-suite. In contrast, spinal testing is not necessarily complete but does reduce the test-suite. We give sufficient conditions on the implementation to guarantee completeness of spinal testing. Finally, we specify and analyze an example regarding the Ceiling Speed Monitoring Function from the European Train Control System. (C) 2016 The Author(s). Published by Elsevier Inc.
|
|
| 13. |
- Caltais, Georgiana, et al.
(författare)
-
(De-)Composing Causality in Labeled Transition Systems
- 2016
-
Ingår i: 1st Workshop on Causal Reasoning for Embedded and safety-critical Systems Technologies (CREST’16). - : Open Publishing Association. ; , s. 10-24
-
Konferensbidrag (refereegranskat)abstract
- In this paper we introduce a notion of counterfactual causality in the Halpern and Pearl sense that is compositional with respect to the interleaving of transition systems. The formal framework for reasoning on what caused the violation of a safety property is established in the context of labeled transition systems and Hennessy Milner logic. The compositionality results are devised for non-communicating systems.
|
|
| 14. |
|
|
| 15. |
|
|
| 16. |
- Costa Paiva, Sofia, et al.
(författare)
-
Complete IOCO Test Cases : A Case Study
- 2016
-
Ingår i: A-TEST 2016 - Proceedings of the 7th International Workshop on Automating Test Case Design, Selection, and Evaluation, co-located with FSE 2016. - New York, NY : ACM Press. - 9781450344012 ; , s. 38-44
-
Konferensbidrag (refereegranskat)abstract
- Input/Output Transition Systems (IOTSs) have been widely used as test models in model-based testing. Traditionally, input output conformance testing (IOCO) has been used to generate random test cases from IOTSs. A recent test case generation method for IOTSs, called Complete IOCO, applies fault models to obtain complete test suites with guaranteed fault coverage for IOTSs. This paper measures the efficiency of Complete IOCO in comparison with the traditional IOCO test case generation implemented in the JTorX tool. To this end, we use a case study involving five specification models from the automotive and the railway domains. Faulty mutations of the specifications were produced in order to compare the efficiency of both test generation methods in killing them. The results indicate that Complete IOCO is more efficient in detecting deep faults in large state spaces while IOCO is more efficient in detecting shallow faults in small state spaces. © 2016 ACM.
|
|
| 17. |
|
|
| 18. |
- Fragal, Vanderson Hafemann, et al.
(författare)
-
Reducing the Concretization Effort in FSM-Based Testing of Software Product Lines
- 2017
-
Ingår i: 10th IEEE International Conference on Software Testing, Verification and Validation Workshops - ICSTW 2017. - Los Alamitos, CA : IEEE. - 9781509066766 - 9781509066773 ; , s. 329-336
-
Konferensbidrag (refereegranskat)abstract
- To test a Software Product Line (SPL), the test artifacts and the techniques must be extended to support variability. In general, when new SPL products are developed, more tests are generated to cover new or modified features. A dominant source of extra effort for such tests is the concretization of newly generated tests. Thus, minimizing the amount of new non-concretized tests required to perform conformance testing on new products reduces the overall test effort. In this paper, we propose a test reuse strategy for conformance testing of SPL products that aims at reducing test effort. We use incremental test generation methods based on finite state machines (FSMs) to maximize test reuse. We combine these methods with a selection algorithm used to identify non-redundant concretized tests. We illustrate our strategy using examples and a case study with an embedded mobile SPL. The results indicate that our strategy can save up to 36% of test effort in comparison to current test reuse strategies for the same fault detection capability. © 2017 IEEE.
|
|
| 19. |
- Fragal, Vanderson Hafemann, et al.
(författare)
-
Validated Test Models for Software Product Lines : Featured Finite State Machines
- 2016
-
Ingår i: Formal Aspects of Component Software. - Cham : Springer. - 9783319576657 - 9783319576664 ; , s. 210-227
-
Konferensbidrag (refereegranskat)abstract
- Variants of the finite state machine (FSM) model have been extensively used to describe the behaviour of reactive systems. In particular, several model-based testing techniques have been developed to support test case generation and test case executions from FSMs. Most such techniques require several validation properties to hold for the underlying test models. In this paper, we propose an extension of the FSM test model for software product lines (SPLs), named featured finite state machine (FFSM). As the first step towards using FFSMs as test models, we define feature-oriented variants of basic test model validation criteria. We show how the high-level validation properties coincide with the necessary properties on the product FSMs. Moreover, we provide a mechanised tool prototype for checking the feature-oriented properties using satisfiability modulo theory (SMT) solver tools. We investigate the applicability of our approach by applying it to both randomly generated FFSMs as well as those from a realistic case study (the Body Comfort System). The results of our study show that for random FFSMs over 16 independent non-mandatory features, our technique provides substantial efficiency gains for the set of proposed validity checks. © Springer International Publishing AG 2017
|
|
| 20. |
- Ghassemi, Fatemeh, et al.
(författare)
-
Product Line Process Theory
- 2016
-
Ingår i: The Journal of logical and algebraic methods in programming. - Amsterdam : Elsevier. - 2352-2208 .- 2352-2216. ; 85:1, part 2, s. 200-226
-
Tidskriftsartikel (refereegranskat)abstract
- Software product lines (SPLs) facilitate reuse and customization in software development by genuinely addressing the concept of variability. Product Line Calculus of Communicating Systems (PL-CCS) is a process calculus for behavioral modeling of SPLs, in which variability can be explicitly modeled by a binary variant operator. In this paper, we study different notions of behavioral equivalence for PL-CCS, based on Park and Milner's strong bisimilarity. These notions enable reasoning about the behavior of SPLs at different levels of abstraction. We study the compositionality property of these notions and the mutual relationship among them. We further show how the strengths of these notions can be consolidated in an equational reasoning method. Finally, we designate the notions of behavioral equivalence that are characterized by the property specification language for PL-CCS, called multi-valued modal μ-calculus. © 2015 The Authors. Published by Elsevier Inc.
|
|
