hh.sePublications
Change search
Link to record
Permanent link

Direct link
Beohar, Harsh
Publications (8 of 8) Show all publications
Varshosaz, M., Beohar, H. & Mousavi, M. R. (2018). Basic Behavioral Models For Software Product Lines: Revisited. Science of Computer Programming, 168, 171-185
Open this publication in new window or tab >>Basic Behavioral Models For Software Product Lines: Revisited
2018 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 168, p. 171-185Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Amsterdam: Elsevier, 2018
Keywords
Software product lines, Behavioral model, Featured transition systems, Calculus of communicating systems, Product line labeled transition systems
National Category
Embedded Systems
Identifiers
urn:nbn:se:hh:diva-33892 (URN)10.1016/j.scico.2018.09.001 (DOI)000450385200010 ()2-s2.0-85054040481 (Scopus ID)
Projects
AUTO-CAAS HoG
Funder
Knowledge Foundation, 20140312Swedish Research Council, 621-2014-5057ELLIIT - The Linköping‐Lund Initiative on IT and Mobile Communications
Available from: 2017-05-26 Created: 2017-05-26 Last updated: 2021-05-06Bibliographically approved
Beohar, H., Varshosaz, M. & Mousavi, M. R. (2016). Basic behavioral models for software product lines: Expressiveness and testing pre-orders. Paper presented at 29th Symposium On Applied Computing, Gyeongju, South Korea, March 24-28, 2014. Science of Computer Programming, 123, 42-60
Open this publication in new window or tab >>Basic behavioral models for software product lines: Expressiveness and testing pre-orders
2016 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 123, p. 42-60Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Amsterdam: Elsevier, 2016
Keywords
Software product lines, Formal specification, Behavioral specification, Labeled transition systems, Featured transition systems, Modal transition systems, Calculus of communicating systems (CCS), Product line CCS (PL-CCS)
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-29104 (URN)10.1016/j.scico.2015.06.005 (DOI)000374367600003 ()2-s2.0-84937604468 (Scopus ID)
Conference
29th Symposium On Applied Computing, Gyeongju, South Korea, March 24-28, 2014
Projects
EFFEMBAC
Funder
Swedish Research Council, 621-2014-5057Knowledge Foundation, 20140312
Note

Issue with selected and extended papers from ACM SVT 2014.

Available from: 2015-08-10 Created: 2015-08-10 Last updated: 2021-05-06Bibliographically approved
Beohar, H. & Mousavi, M. R. (2016). Input–output conformance testing for software product lines. The Journal of logical and algebraic methods in programming, 85(6), 1131-1153
Open this publication in new window or tab >>Input–output conformance testing for software product lines
2016 (English)In: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, Vol. 85, no 6, p. 1131-1153Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Amsterdam: Elsevier, 2016
Keywords
Model based testing, Input–output conformance testing, Software product lines, Input–output featured transition systems
National Category
Software Engineering
Identifiers
urn:nbn:se:hh:diva-33621 (URN)10.1016/j.jlamp.2016.09.007 (DOI)000388062000003 ()2-s2.0-85008682089 (Scopus ID)
Projects
AUTO-CAAS, KK HÖG ProjectEFFEMBAC, VR Project
Funder
ELLIIT - The Linköping‐Lund Initiative on IT and Mobile CommunicationsKnowledge Foundation, 20140312Swedish Research Council, 621-2014-5057
Available from: 2017-03-27 Created: 2017-03-27 Last updated: 2018-03-23Bibliographically approved
Beohar, H. & Mousavi, M. R. (2015). A Pre-congruence Format for XY-simulation. In: Mehdi Dastani & Marjan Sirjani (Ed.), Fundamentals of Software Engineering: 6th International Conference, FSEN 2015 Tehran, Iran, April 22–24, 2015, Revised Selected Papers. Paper presented at The 6th IPM International Conference on Fundamentals of Software Engineering (FSEN 2015), Tehran, Iran, 22-24 April, 2015 (pp. 215-229). Cham: Springer, 9392
Open this publication in new window or tab >>A Pre-congruence Format for XY-simulation
2015 (English)In: Fundamentals of Software Engineering: 6th International Conference, FSEN 2015 Tehran, Iran, April 22–24, 2015, Revised Selected Papers / [ed] Mehdi Dastani & Marjan Sirjani, Cham: Springer, 2015, Vol. 9392, p. 215-229Conference paper, Published paper (Refereed)
Abstract [en]

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

Place, publisher, year, edition, pages
Cham: Springer, 2015
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9392
Keywords
Structural Operational Semantics, Rule Formats, Pre-Congruence, XY-Simulation
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-29103 (URN)10.1007/978-3-319-24644-4_15 (DOI)000366208800015 ()2-s2.0-84950326879 (Scopus ID)978-3-319-24643-7 (ISBN)978-3-319-24644-4 (ISBN)
Conference
The 6th IPM International Conference on Fundamentals of Software Engineering (FSEN 2015), Tehran, Iran, 22-24 April, 2015
Projects
EFFEMBAC ( (Effective Model-Based Testing of Concurrent Systems)
Funder
Swedish Research Council, 621-2014-5057ELLIIT - The Linköping‐Lund Initiative on IT and Mobile Communications
Available from: 2015-08-10 Created: 2015-08-10 Last updated: 2018-03-22Bibliographically approved
Varshosaz, M., Beohar, H. & Mousavi, M. R. (2015). Delta-Oriented FSM-Based Testing. In: Michael Butler, Sylvain Conchon & Fatiha Zaïdi (Ed.), Formal Methods and Software Engineering: 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings. Paper presented at 17th International Conference on Formal Engineering Methods (ICFEM 2015), Paris, France, November 3-5, 2015 (pp. 366-381). Cham: Springer, 9407
Open this publication in new window or tab >>Delta-Oriented FSM-Based Testing
2015 (English)In: Formal Methods and Software Engineering: 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings / [ed] Michael Butler, Sylvain Conchon & Fatiha Zaïdi, Cham: Springer, 2015, Vol. 9407, p. 366-381Conference paper, Published paper (Refereed)
Abstract [en]

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

Place, publisher, year, edition, pages
Cham: Springer, 2015
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9407
Keywords
Model-Based Testing, FSM-based Testing, HSI Method, Software Product Lines, Delta-Oriented Programming, DeltaJava
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:hh:diva-29999 (URN)10.1007/978-3-319-25423-4_24 (DOI)2-s2.0-84949239517 (Scopus ID)978-3-319-25422-7 (ISBN)978-3-319-25423-4 (ISBN)
Conference
17th International Conference on Formal Engineering Methods (ICFEM 2015), Paris, France, November 3-5, 2015
Projects
EFFEMBACAUTO-CAAS
Funder
ELLIIT - The Linköping‐Lund Initiative on IT and Mobile CommunicationsSwedish Research Council, 621-2014-5057Knowledge Foundation
Note

M.R. Mousavi—The work has been partially supported by the Swedish Research Council award number: 621-2014-5057 and the Swedish Knowledge Foundation in the context of the AUTO-CAAS HöG project.

Available from: 2015-12-09 Created: 2015-12-09 Last updated: 2021-05-06Bibliographically approved
Beohar, H. & Cuijpers, P. (2014). Avoiding Diamonds in Desynchronisation. Paper presented at 9th International Symposium on Formal Aspects of Component Software (FACS), Mountain View, CA, USA, September 12-14, 2012. Science of Computer Programming, 91(PART A), 45-69
Open this publication in new window or tab >>Avoiding Diamonds in Desynchronisation
2014 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 91, no PART A, p. 45-69Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Amsterdam: Elsevier, 2014
Keywords
Synchrony to asynchrony, Desynchronisation, Branching bisimulation, Equivalence checking of infinite state systems
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-24984 (URN)10.1016/j.scico.2013.12.002 (DOI)000338401300003 ()2-s2.0-84901613572 (Scopus ID)
Conference
9th International Symposium on Formal Aspects of Component Software (FACS), Mountain View, CA, USA, September 12-14, 2012
Projects
“Integrated Multi-formalism Tool Support for the Design of Networked Embedded Control Systems” (MULTIFORM) project
Funder
EU, FP7, Seventh Framework Programme, INFSO-ICT-224249
Available from: 2014-04-05 Created: 2014-04-05 Last updated: 2022-07-06Bibliographically approved
Beohar, H. & Mousavi, M. R. (2014). Input-output conformance testing based on featured transition systems. In: Proceedings of the 29th Annual ACM Symposium on Applied Computing: . Paper presented at 29th Annual ACM Symposium on Applied Computing, SAC 2014, March 24-28 2017, Gyeongju, South Korea (pp. 1272-1278). Association for Computing Machinery (ACM)
Open this publication in new window or tab >>Input-output conformance testing based on featured transition systems
2014 (English)In: Proceedings of the 29th Annual ACM Symposium on Applied Computing, Association for Computing Machinery (ACM), 2014, p. 1272-1278Conference paper, Published paper (Refereed)
Abstract [en]

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

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2014
Keywords
Computer software, Input-output; Input-output conformance; Model based testing; Product configuration; Refinement operators; Software Product Line; Test case; Transition system, Model checking
National Category
Software Engineering
Identifiers
urn:nbn:se:hh:diva-36572 (URN)10.1145/2554850.2554949 (DOI)2-s2.0-84905641858 (Scopus ID)978-1-4503-2469-4 (ISBN)
Conference
29th Annual ACM Symposium on Applied Computing, SAC 2014, March 24-28 2017, Gyeongju, South Korea
Available from: 2018-05-02 Created: 2018-05-02 Last updated: 2018-05-02Bibliographically approved
Beohar, H. & Mousavi, M. R. (2014). Spinal test suites for software product lines. In: Alexander K. Petrenko, Holger Schlingloff (Ed.), Proceedings: Ninth Workshop on Model-Based Testing (MBT 2014). Paper presented at Conference of 9th Workshop on Model-Based Testing, (MBT 2014), Grenoble, France, April 6, 2014 (pp. 44-55). Sydney: Open Publishing Association, 141
Open this publication in new window or tab >>Spinal test suites for software product lines
2014 (English)In: Proceedings: Ninth Workshop on Model-Based Testing (MBT 2014) / [ed] Alexander K. Petrenko, Holger Schlingloff, Sydney: Open Publishing Association , 2014, Vol. 141, p. 44-55Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Sydney: Open Publishing Association, 2014
Series
Electronic Proceedings in Theoretical Computer Science, E-ISSN 2075-2180 ; 141
Keywords
Computer software, Model checking, Software design, Conformance testing, Formal theory, Input-output conformance, Model based testing, Novel concept, Software Product Line, Testing software, Transition system, Software testing
National Category
Software Engineering
Identifiers
urn:nbn:se:hh:diva-40223 (URN)10.4204/EPTCS.141.4 (DOI)2-s2.0-84939638773 (Scopus ID)
Conference
Conference of 9th Workshop on Model-Based Testing, (MBT 2014), Grenoble, France, April 6, 2014
Available from: 2019-07-12 Created: 2019-07-12 Last updated: 2019-08-13Bibliographically approved
Organisations

Search in DiVA

Show all publications