| 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. |
|
|
| 3. |
- Aerts, Arend, et al.
(författare)
-
A Tool Prototype for Model-Based Testing of Cyber-Physical Systems
- 2015
-
Ingår i: Theoretical Aspects of Computing – ICTAC 2015. - Cham : Springer. - 9783319251493 - 9783319251509 ; , s. 563-572
-
Konferensbidrag (refereegranskat)abstract
- We report on a tool prototype for model-based testing of cyber-physical systems. Our starting point is a hybrid-system model specified in a domain-specific language called Acumen. Our prototype tool is implemented in Matlab and covers three stages of model-based testing, namely, test-case generation, test-case execution, and conformance analysis. We have applied our implementation to a number of typical examples of cyber-physical systems in order to analyze its applicability. In this paper, we report on the result of applying the prototype tool on a DC-DC boost converter. © Springer International Publishing Switzerland 2015
|
|
| 4. |
- Aerts, Arend, et al.
(författare)
-
Model-Based Testing of Cyber-Physical Systems
- 2016
-
Ingår i: Cyber-Physical Systems. - Saint Louis : Elsevier. - 9780128038017 ; , s. 287-304
-
Bokkapitel (refereegranskat)abstract
- Cyber-physical systems (CPSs) are the result of the integration of connected computer systems with the physical world. They feature complex interactions that go beyond traditional communication schemes and protocols in computer systems. One distinguished feature of such complex interactions is the tight coupling between discrete and continuous interactions, captured by hybrid system models.Due to the complexity of CPSs, providing rigorous and model-based analysis methods and tools for verifying correctness of such systems is of the utmost importance. Model-based testing (MBT) is one such verification technique that can be used for checking the conformance of an implementation of a system to its specification (model).In this chapter, we first review the main concepts and techniques in MBT. Subsequently, we review the most common modeling formalisms for CPSs, with focus on hybrid system models. Subsequently, we provide a brief overview of conformance relations and conformance testing techniques for CPSs. © 2017 Elsevier Inc. All rights reserved.
|
|
| 5. |
- Aichernig, Bernhard K., et al.
(författare)
-
Model Learning and Model-Based Testing
- 2018
-
Ingår i: Machine Learning for Dynamic Software Analysis. - Heidelberg : Springer. - 9783319965611 - 9783319965628 ; , s. 74-100
-
Konferensbidrag (refereegranskat)abstract
- We present a survey of the recent research efforts in integrating model learning with model-based testing. We distinguished two strands of work in this domain, namely test-based learning (also called test-based modeling) and learning-based testing. We classify the results in terms of their underlying models, their test purpose and techniques, and their target domains. © Springer International Publishing AG
|
|
| 6. |
- 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
|
|
| 7. |
- Araujo, Hugo, et al.
(författare)
-
A Process for Sound Conformance Testing of Cyber-Physical Systems
- 2017
-
Ingår i: 2017 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). - Los Alamitos, CA : IEEE Computer Society. - 9781509066766 - 9781509066773 ; , s. 46-50
-
Konferensbidrag (refereegranskat)abstract
- We present a process for sound conformance testing of cyber-physical systems, which involves functional but also non-functional aspects. The process starts with a hybrid model of cyber-physical systems in which the correct behavior of the system (at its interface level) is specified. Such a model captures both discrete behavior and evolution of continuous dynamics of the system in time. Since conformance testing inherently involves comparing continuous dynamics, the key parameters of the process are (1) the conformance bounds defining when two signals are sufficiently close to each other, and (2) the permitted error margin in the conformance analysis introduced by sampling of continuous signals. The final parameter of this process is (3) finding (and adjusting) the sampling rate of the dynamic behavior. In the specified process, we provide different alternatives for fixing the error margin of the conformance testing if the sampling rate is fixed, establishing the sampling rate if the error margin is fixed and finding conformance bounds once the sampling rate and the error margin are fixed. © 2017 IEEE.
|
|
| 8. |
- 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.
|
|
| 9. |
- Arts, Thomas, et al.
(författare)
-
Automatic Consequence Analysis of Automotive Standards (AUTO-CAAS) [Position Paper]
- 2015
-
Ingår i: WASA '15. - New York, NY : ACM Press. - 9781450334440 ; , s. 35-38
-
Konferensbidrag (refereegranskat)abstract
- This paper provides some background and the roadmap of the AUTO-CAAS project, which is a 3-year project financed by the Swedish Knowledge Foundation and is ongoing as a joint project among three academic and industrial partners. The aim of the project is to exploit the formal models of the AUTOSAR standard, developed by the industrial partner of the project Quviq AB, in order to predict possible future failures in concrete implementations of components. To this end, the deviations from the formal specification will be exploited to generate test-cases that can push concrete components to the corners where such deviation will result in observable failures. The same information will also be used in the diagnosis of otherwise detected failures in order to pinpoint their root causes.
|
|
| 10. |
- Beohar, Harsh, 1984-, et al.
(författare)
-
A Pre-congruence Format for XY-simulation
- 2015
-
Ingår i: Fundamentals of Software Engineering. - Cham : Springer. - 9783319246437 - 9783319246444 ; , s. 215-229
-
Konferensbidrag (refereegranskat)abstract
- XY-simulation is a generalization of bisimulation that is parameterized with two subsets of actions. XY-simulation is known in the literature under different names such as modal refinement, partial bisimulation, and alternating simulation. In this paper, we propose a precongruence rule format for XY-simulation. The format allows for checking compositionality of XY-simulation for an arbitrary language with structural operational semantics, by performing very simple checks on the syntactic shape of the rules. We apply our format to derive concrete compositionality results for different notions of behavioral pre-order with respect to different process calculi in the literature. © IFIP International Federation for Information Processing 2015
|
|
