| 1. |
- 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
|
|
| 2. |
- Beohar, Harsh, 1984-, et al.
(författare)
-
Avoiding Diamonds in Desynchronisation
- 2014
-
Ingår i: Science of Computer Programming. - Amsterdam : Elsevier. - 0167-6423 .- 1872-7964. ; 91:PART A, s. 45-69
-
Tidskriftsartikel (refereegranskat)abstract
- The design of concurrent systems often assumes synchronous communication between different parts of a system. When system components are physically apart, this assumption becomes inappropriate. Desynchronisation is a technique that aims to implement a synchronous design in an asynchronous manner by placing buffers between the components of the synchronous design. When queues are used as buffers, the so-called 'diamond property' (among others) ensures correct operation of the desynchronised design. However, this property is difficult to establish in practice. In this paper, we give sufficient and necessary conditions under which a concrete synchronous design (i.e., without the unobservable action) is equivalent to an asynchronous design and formally prove that the diamond property is no longer needed for desynchronisation when half-duplex queues are used as a communication buffer. Furthermore, we discuss how the half-duplex condition can be further relaxed when the diamond property can be partially guaranteed. To illustrate how this theory may be applied, we desynchronise the synchronous systems that are synthesised using supervisory control theory. © 2013 Elsevier B.V.
|
|
| 3. |
- 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.
|
|
| 4. |
- Beohar, Harsh, 1984-, et al.
(författare)
-
Input-output conformance testing based on featured transition systems
- 2014
-
Ingår i: Proceedings of the 29th Annual ACM Symposium on Applied Computing. - New York, NY, USA : Association for Computing Machinery (ACM). - 9781450324694 ; , s. 1272-1278
-
Konferensbidrag (refereegranskat)abstract
- We extend the theory of input-output conformance testing to the setting of software product lines. In particular, we allow for input-output featured transition systems to be used as the basis for generating test suites and test cases. We introduce refinement operators both at the level of models and at the level of test suites that allow for projecting them into a specific product configuration (or a product sub-line). We show that the two sorts of refinement are consistent and lead to the same set of test-cases. © Copyright 2014 ACM
|
|
| 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. |
- Beohar, Harsh, 1984-, et al.
(författare)
-
Spinal test suites for software product lines
- 2014
-
Ingår i: Proceedings. - Sydney : Open Publishing Association. ; , s. 44-55
-
Konferensbidrag (refereegranskat)abstract
- A major challenge in testing software product lines is efficiency. In particular, testing a product line should take less effort than testing each and every product individually. We address this issue in the context of input-output conformance testing, which is a formal theory of model-based testing. We extend the notion of conformance testing on input-output featured transition systems with the novel concept of spinal test suites. We show how this concept dispenses with retesting the common behavior among different, but similar, products of a software product line. © H. Beohar & M.R. Mousavi.
|
|
| 7. |
- Varshosaz, Mahsa, 1985-, et al.
(författare)
-
Basic Behavioral Models For Software Product Lines : Revisited
- 2018
-
Ingår i: Science of Computer Programming. - Amsterdam : Elsevier. - 0167-6423 .- 1872-7964. ; 168, s. 171-185
-
Tidskriftsartikel (refereegranskat)abstract
- In Beohar et al. (2016) [9], we established an expressiveness hierarchy and studied the notions of refinement and testing for three fundamental behavioral models for software product lines. These models were featured transition systems, product line labeled transition systems, and modal transition systems. It turns out that our definition of product line labeled transition systems is more restrictive than the one introduced by Gruler, Leucker, and Scheidemann. Adopting the original and more liberal notion changes the expressiveness results, as we demonstrate in this paper. Namely, we show that the original notion of product line labeled transition systems and featured transition systems are equally expressive. As an additional result, we show that there are featured transition systems for which the size of the corresponding product line labeled transition system, resulting from any sound encoding, is exponentially larger than the size of the original model. Furthermore, we show that each product line labeled transition system can be encoded into a featured transition system, such that the size of featured transition system is linear in terms of the size of the corresponding model. To summarize, featured transition systems are equally expressive as, but exponentially more succinct than, product line labeled transition systems. © 2018 Elsevier B.V.
|
|
| 8. |
- Varshosaz, Mahsa, 1985-, et al.
(författare)
-
Delta-Oriented FSM-Based Testing
- 2015
-
Ingår i: Formal Methods and Software Engineering. - Cham : Springer. - 9783319254227 - 9783319254234 ; , s. 366-381
-
Konferensbidrag (refereegranskat)abstract
- We use the concept of delta-oriented programming to organize FSM-based test models in an incremental structure. We then exploit incremental FSM-based testing to make efficient use of this high-level structure in generating test cases. We show how our approach can lead to more efficient test-case generation, both by analyzing the complexity of the test-case generation algorithm and by applying the technique to a case study. © Springer International Publishing Switzerland 2015
|
|
