| 1. |
- Khamespanah, Ehsan, et al.
(författare)
-
State Distribution Policy for Distributed Model Checking of Actor Models
- 2015
-
Ingår i: Electronic Communications of the EASST. - Berlin : Universitätsverlag der TU Berlin. - 1863-2122. ; 72, s. 1-15
-
Tidskriftsartikel (refereegranskat)abstract
- Model checking temporal properties is often reduced to finding accepting cycles in Büchi automata. A key ingredient for an effective distributed model checking technique is a distribution policy that does not split the potential accepting cycles of the corresponding automaton among several nodes. In this paper, we introduce a distribution policy to reduce the number of split cycles. This policy is based on the call dependency graph, obtained from the message passing skeleton of the model. We prove theoretical results about the correspondence between the cycles of call dependency graph and the cycles of the concrete state space and provide empirical data obtained from applying our distribution policy in state space generation and reachability analysis. We take Rebeca, an imperative interpretation of actors, as our modeling language and implement the introduced policy in its distributed state space generator. Our technique can be applied to other message-driven actor-based models where concurrent objects or services are units of concurrency.
|
|
| 2. |
- Ali, Nauman bin, et al.
(författare)
-
On the search for industry-relevant regression testing research
- 2019
-
Ingår i: Empirical Software Engineering. - New York, NY : Springer. - 1382-3256 .- 1573-7616. ; 24:4, s. 2020-2055
-
Tidskriftsartikel (refereegranskat)abstract
- Regression testing is a means to assure that a change in the software, or its execution environment, does not introduce new defects. It involves the expensive undertaking of rerunning test cases. Several techniques have been proposed to reduce the number of test cases to execute in regression testing, however, there is no research on how to assess industrial relevance and applicability of such techniques. We conducted a systematic literature review with the following two goals: firstly, to enable researchers to design and present regression testing research with a focus on industrial relevance and applicability and secondly, to facilitate the industrial adoption of such research by addressing the attributes of concern from the practitioners' perspective. Using a reference-based search approach, we identified 1068 papers on regression testing. We then reduced the scope to only include papers with explicit discussions about relevance and applicability (i.e. mainly studies involving industrial stakeholders). Uniquely in this literature review, practitioners were consulted at several steps to increase the likelihood of achieving our aim of identifying factors important for relevance and applicability. We have summarised the results of these consultations and an analysis of the literature in three taxonomies, which capture aspects of industrial-relevance regarding the regression testing techniques. Based on these taxonomies, we mapped 38 papers reporting the evaluation of 26 regression testing techniques in industrial settings. © The Author(s) 2019
|
|
| 3. |
- Araujo, Hugo, et al.
(författare)
-
Sound conformance testing for cyber-physical systems : Theory and implementation
- 2018
-
Ingår i: Science of Computer Programming. - Amsterdam : ELSEVIER SCIENCE BV. - 0167-6423 .- 1872-7964. ; 162, s. 35-54
-
Tidskriftsartikel (refereegranskat)abstract
- Conformance testing is a formal and structured approach to verifying system correctness. We propose a conformance testing algorithm for cyber-physical systems, based on the notion of hybrid conformance by Abbas and Fainekos. We show how the dynamics of system specification and the sampling rate play an essential role in making sound verdicts. We specify and prove error bounds that lead to sound test-suites for a given specification and a given sampling rate. We use reachability analysis to find such bounds and implement the proposed approach using the CORA toolbox in Matlab. We apply the implemented approach on a case study from the automotive domain.
|
|
| 4. |
- 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.
|
|
| 5. |
- 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.
|
|
| 6. |
|
|
| 7. |
|
|
| 8. |
- Entekhabi, Sina, 1989-, et al.
(författare)
-
Automated and Efficient Test-Generation for Grid-Based Multiagent Systems : Comparing Random Input Filtering versus Constraint Solving
- 2023
-
Ingår i: ACM Transactions on Software Engineering and Methodology. - New York, NY : Association for Computing Machinery (ACM). - 1049-331X .- 1557-7392. ; 33:1
-
Tidskriftsartikel (refereegranskat)abstract
- Automatic generation of random test inputs is an approach that can alleviate the challenges of manual test case design. However, random test cases may be ineffective in fault detection and increase testing cost, especially in systems where test execution is resource- and time-consuming. To remedy this, the domain knowledge of test engineers can be exploited to select potentially effective test cases. To this end, test selection constraints suggested by domain experts can be utilized either for filtering randomly generated test inputs or for direct generation of inputs using constraint solvers. In this article, we propose a domain specific language (DSL) for formalizing locality-based test selection constraints of autonomous agents and discuss the impact of test selection filters, specified in our DSL, on randomly generated test cases. We study and compare the performance of filtering and constraint solving approaches in generating selective test cases for different test scenario parameters and discuss the role of these parameters in test generation performance. Through our study, we provide criteria for suitability of the random data filtering approach versus the constraint solving one under the varying size and complexity of our testing problem. We formulate the corresponding research questions and answer them by designing and conducting experiments using QuickCheck for random test data generation with filtering and Z3 for constraint solving. Our observations and statistical analysis indicate that applying filters can significantly improve test efficiency of randomly generated test cases. Furthermore, we observe that test scenario parameters affect the performance of the filtering and constraint solving approaches differently. In particular, our results indicate that the two approaches have complementary strengths: random generation and filteringworks best for large agent numbers and long paths, while its performance degrades in the larger grid sizes and more strict constraints. On the contrary, constraint solving has a robust performance for large grid sizes and strict constraints, while its performance degrades with more agents and long paths. © 2023 Copyright held by the owner/author(s).
|
|
| 9. |
- 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.
|
|
| 10. |
|
|
