Showing 1–21 of 21 results for author: Maoz, S

Shelving it rather than Ditching it: Dynamically Debloating DEX and Native Methods of Android Applications without APK Modification

Authors: Zicheng Zhang, Jiakun Liu, Ferdian Thung, Haoyu Ma, Rui Li, Yan Naing Tun, Wei Minn, Lwin Khin Shar, Shahar Maoz, Eran Toch, David Lo, Joshua Wong, Debin Gao

Abstract: Today's Android developers tend to include numerous features to accommodate diverse user requirements, which inevitably leads to bloated apps. Yet more often than not, only a fraction of these features are frequently utilized by users, thus a bloated app costs dearly in potential vulnerabilities, expanded attack surfaces, and additional resource consumption. Especially in the event of severe secur… ▽ More Today's Android developers tend to include numerous features to accommodate diverse user requirements, which inevitably leads to bloated apps. Yet more often than not, only a fraction of these features are frequently utilized by users, thus a bloated app costs dearly in potential vulnerabilities, expanded attack surfaces, and additional resource consumption. Especially in the event of severe security incidents, users have the need to block vulnerable functionalities immediately. Existing works have proposed various code debloating approaches for identifying and removing features of executable components. However, they typically involve static modification of files (and, for Android apps, repackaging of APKs, too), which lacks user convenience let alone undermining the security model of Android due to the compromising of public key verification and code integrity checks. This paper introduces 3DNDroid, a Dynamic Debloating approach targeting both DEX and Native methods in AnDroid apps. Using an unprivileged management app in tandem with a customized Android OS, 3DNDroid dynamically reduces unnecessary code loading during app execution based on a pre-generated debloating schema from static or dynamic analyses. It intercepts invocations of debloated bytecode methods to prevent their interpretation, compilation, and execution, while zero-filling memory spaces of debloated native methods during code loading. Evaluation demonstrates 3DNDroid's ability to debloat 187 DEX methods and 30 native methods across 55 real-world apps, removing over 10K Return-Oriented Programming (ROP) gadgets. Case studies confirm its effectiveness in mitigating vulnerabilities, and performance assessments highlight its resource-saving advantages over non-debloated apps. △ Less

Submitted 8 January, 2025; originally announced January 2025.

Kernelization Complexity of Solution Discovery Problems

Authors: Mario Grobler, Stephanie Maaz, Amer E. Mouawad, Naomi Nishimura, Vijayaragunathan Ramamoorthi, Sebastian Siebertz

Abstract: In the solution discovery variant of a vertex (edge) subset problem $Π$ on graphs, we are given an initial configuration of tokens on the vertices (edges) of an input graph $G$ together with a budget $b$. The question is whether we can transform this configuration into a feasible solution of $Π$ on $G$ with at most $b$ modification steps. We consider the token sliding variant of the solution disco… ▽ More In the solution discovery variant of a vertex (edge) subset problem $Π$ on graphs, we are given an initial configuration of tokens on the vertices (edges) of an input graph $G$ together with a budget $b$. The question is whether we can transform this configuration into a feasible solution of $Π$ on $G$ with at most $b$ modification steps. We consider the token sliding variant of the solution discovery framework, where each modification step consists of sliding a token to an adjacent vertex (edge). The framework of solution discovery was recently introduced by Fellows et al. [Fellows et al., ECAI 2023] and for many solution discovery problems the classical as well as the parameterized complexity has been established. In this work, we study the kernelization complexity of the solution discovery variants of Vertex Cover, Independent Set, Dominating Set, Shortest Path, Matching, and Vertex Cut with respect to the parameters number of tokens $k$, discovery budget $b$, as well as structural parameters such as pathwidth. △ Less

Submitted 25 September, 2024; originally announced September 2024.

Solution discovery via reconfiguration for problems in P

Authors: Mario Grobler, Stephanie Maaz, Nicole Megow, Amer E. Mouawad, Vijayaragunathan Ramamoorthi, Daniel Schmand, Sebastian Siebertz

Abstract: In the recently introduced framework of solution discovery via reconfiguration [Fellows et al., ECAI 2023], we are given an initial configuration of $k$ tokens on a graph and the question is whether we can transform this configuration into a feasible solution (for some problem) via a bounded number $b$ of small modification steps. In this work, we study solution discovery variants of polynomial-ti… ▽ More In the recently introduced framework of solution discovery via reconfiguration [Fellows et al., ECAI 2023], we are given an initial configuration of $k$ tokens on a graph and the question is whether we can transform this configuration into a feasible solution (for some problem) via a bounded number $b$ of small modification steps. In this work, we study solution discovery variants of polynomial-time solvable problems, namely Spanning Tree Discovery, Shortest Path Discovery, Matching Discovery, and Vertex/Edge Cut Discovery in the unrestricted token addition/removal model, the token jumping model, and the token sliding model. In the unrestricted token addition/removal model, we show that all four discovery variants remain in P. For the toking jumping model we also prove containment in P, except for Vertex/Edge Cut Discovery, for which we prove NP-completeness. Finally, in the token sliding model, almost all considered problems become NP-complete, the exception being Spanning Tree Discovery, which remains polynomial-time solvable. We then study the parameterized complexity of the NP-complete problems and provide a full classification of tractability with respect to the parameters solution size (number of tokens) $k$ and transformation budget (number of steps) $b$. Along the way, we observe strong connections between the solution discovery variants of our base problems and their (weighted) rainbow variants as well as their red-blue variants with cardinality constraints. △ Less

Submitted 22 November, 2023; originally announced November 2023.

Parameterized complexity of reconfiguration of atoms

Authors: Alexandre Cooper, Stephanie Maaz, Amer E. Mouawad, Naomi Nishimura

Abstract: Our work is motivated by the challenges presented in preparing arrays of atoms for use in quantum simulation. The recently-developed process of loading atoms into traps results in approximately half of the traps being filled. To consolidate the atoms so that they form a dense and regular arrangement, such as all locations in a grid, atoms are rearranged using moving optical tweezers. Time is of th… ▽ More Our work is motivated by the challenges presented in preparing arrays of atoms for use in quantum simulation. The recently-developed process of loading atoms into traps results in approximately half of the traps being filled. To consolidate the atoms so that they form a dense and regular arrangement, such as all locations in a grid, atoms are rearranged using moving optical tweezers. Time is of the essence, as the longer that the process takes and the more that atoms are moved, the higher the chance that atoms will be lost in the process. Viewed as a problem on graphs, we wish to solve the problem of reconfiguring one arrangement of tokens (representing atoms) to another using as few moves as possible. Because the problem is NP-complete on general graphs as well as on grids, we focus on the parameterized complexity for various parameters, considering both undirected and directed graphs, and tokens with and without labels. For unlabelled tokens, the problem is in FPT when parameterizing by the number of tokens, the number of moves, or the number of moves plus the number of vertices without tokens in either the source or target configuration, but intractable when parameterizing by the difference between the number of moves and the number of differences in the placement of tokens in the source and target configurations. When labels are added to tokens, however, most of the tractability results are replaced by hardness results. △ Less

Submitted 26 July, 2021; originally announced July 2021.

Unrealizable Cores for Reactive Systems Specifications

Authors: Shahar Maoz, Rafi Shalom

Abstract: One of the main challenges of reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system, is to deal with unrealizable specifications. One means to deal with unrealizability, in the context of GR(1), an expressive assume-guarantee fragment of LTL that enables efficient synthesis, is the computation of an unrealizable core, which can be viewed as a fault-localiza… ▽ More One of the main challenges of reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system, is to deal with unrealizable specifications. One means to deal with unrealizability, in the context of GR(1), an expressive assume-guarantee fragment of LTL that enables efficient synthesis, is the computation of an unrealizable core, which can be viewed as a fault-localization approach. Existing solutions, however, are computationally costly, are limited to computing a single core, and do not correctly support specifications with constructs beyond pure GR(1) elements. In this work we address these limitations. First, we present QuickCore, a novel algorithm that accelerates unrealizable core computations by relying on the monotonicity of unrealizability, on an incremental computation, and on additional properties of GR(1) specifications. Second, we present Punch, a novel algorithm to efficiently compute all unrealizable cores of a specification. Finally, we present means to correctly handle specifications that include higher-level constructs beyond pure GR(1) elements. We implemented our ideas on top of Spectra, an open-source language and synthesis environment. Our evaluation over benchmarks from the literature shows that QuickCore is in most cases faster than previous algorithms, and that its relative advantage grows with scale. Moreover, we found that most specifications include more than one core, and that Punch finds all the cores significantly faster than a competing naive algorithm. △ Less

Submitted 27 February, 2021; originally announced March 2021.

Comments: Preprint of ICSE'21 paper

Energy mu-Calculus: Symbolic Fixed-Point Algorithms for omega-Regular Energy Games

Authors: Gal Amram, Shahar Maoz, Or Pistiner, Jan Oliver Ringert

Abstract: $ω$-regular energy games, which are weighted two-player turn-based games with the quantitative objective to keep the energy levels non-negative, have been used in the context of verification and synthesis. The logic of modal $μ$-calculus, when applied over game graphs with $ω… ▽ More $ω$-regular energy games, which are weighted two-player turn-based games with the quantitative objective to keep the energy levels non-negative, have been used in the context of verification and synthesis. The logic of modal $μ$-calculus, when applied over game graphs with $ω$-regular winning conditions, allows defining symbolic algorithms in the form of fixed-point formulas for computing the sets of winning states. In this paper, we introduce energy $μ$-calculus, a multi-valued extension of the $μ$-calculus that serves as a symbolic framework for solving $ω$-regular energy games. Energy $μ$-calculus enables the seamless reuse of existing, well-known symbolic $μ$-calculus algorithms for $ω$-regular games, to solve their corresponding energy augmented variants. We define the syntax and semantics of energy $μ$-calculus over symbolic representations of the game graphs, and show how to use it to solve the decision and the minimum credit problems for $ω$-regular energy games, for both bounded and unbounded energy level accumulations. △ Less

Submitted 18 October, 2020; v1 submitted 1 May, 2020; originally announced May 2020.

Spectra: A Specification Language for Reactive Systems

Authors: Shahar Maoz, Jan Oliver Ringert

Abstract: Spectra is a new specification language for reactive systems, specifically tailored for the context of reactive synthesis. The meaning of Spectra is defined by a translation to a kernel language. Spectra comes with the Spectra Tools, a set of analyses, including a synthesizer to obtain a correct-by-construction implementation, several means for executing the resulting controller, and additional an… ▽ More Spectra is a new specification language for reactive systems, specifically tailored for the context of reactive synthesis. The meaning of Spectra is defined by a translation to a kernel language. Spectra comes with the Spectra Tools, a set of analyses, including a synthesizer to obtain a correct-by-construction implementation, several means for executing the resulting controller, and additional analyses aimed at helping engineers write higher-quality specifications. We present the language and give an overview of the tool set. △ Less

Submitted 14 April, 2019; originally announced April 2019.

Performance Heuristics for GR(1) Synthesis and Related Algorithms

Authors: Elizabeth Firman, Shahar Maoz, Jan Oliver Ringert

Abstract: Reactive synthesis for the GR(1) fragment of LTL has been implemented and studied in many works. In this workshop paper we present and evaluate a list of heuristics to potentially reduce running times for GR(1) synthesis and related algorithms. The list includes early detection of fixed-points and unrealizability, fixed-point recycling, and heuristics for unrealizable core computations. We evaluat… ▽ More Reactive synthesis for the GR(1) fragment of LTL has been implemented and studied in many works. In this workshop paper we present and evaluate a list of heuristics to potentially reduce running times for GR(1) synthesis and related algorithms. The list includes early detection of fixed-points and unrealizability, fixed-point recycling, and heuristics for unrealizable core computations. We evaluate the presented heuristics on SYNTECH15, a total of 78 specifications of 6 autonomous Lego robots, written by 3rd year undergraduate computer science students in a project class we have taught, as well as on several benchmarks from the literature. The evaluation investigates not only the potential of the suggested heuristics to improve computation times, but also the difference between existing benchmarks and the robot's specifications in terms of the effectiveness of the heuristics. △ Less

Submitted 28 November, 2017; originally announced December 2017.

Comments: In Proceedings SYNT 2017, arXiv:1711.10224

Journal ref: EPTCS 260, 2017, pp. 62-80

Symbolic BDD and ADD Algorithms for Energy Games

Authors: Shahar Maoz, Or Pistiner, Jan Oliver Ringert

Abstract: Energy games, which model quantitative consumption of a limited resource, e.g., time or energy, play a central role in quantitative models for reactive systems. Reactive synthesis constructs a controller which satisfies a given specification, if one exists. For energy games a synthesized controller ensures to satisfy not only the safety constraints of the specification but also the quantitative co… ▽ More Energy games, which model quantitative consumption of a limited resource, e.g., time or energy, play a central role in quantitative models for reactive systems. Reactive synthesis constructs a controller which satisfies a given specification, if one exists. For energy games a synthesized controller ensures to satisfy not only the safety constraints of the specification but also the quantitative constraints expressed in the energy game. A symbolic algorithm for energy games, recently presented by Chatterjee et al., is symbolic in its representation of quantitative values but concrete in the representation of game states and transitions. In this paper we present an algorithm that is symbolic both in the quantitative values and in the underlying game representation. We have implemented our algorithm using two different symbolic representations for reactive games, Binary Decision Diagrams (BDD) and Algebraic Decision Diagrams (ADD). We investigate the commonalities and differences of the two implementations and compare their running times on specifications of energy games. △ Less

Submitted 22 November, 2016; originally announced November 2016.

Comments: In Proceedings SYNT 2016, arXiv:1611.07178

Journal ref: EPTCS 229, 2016, pp. 35-54

Synthesizing a Lego Forklift Controller in GR(1): A Case Study

Authors: Shahar Maoz, Jan Oliver Ringert

Abstract: Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given specification. GR(1) is a well-known fragment of linear temporal logic (LTL) where synthesis is possible using a polynomial symbolic algorithm. We conducted a case study to learn about the challenges that software engineers may face when using GR(1) synthesis for the development of a rea… ▽ More Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given specification. GR(1) is a well-known fragment of linear temporal logic (LTL) where synthesis is possible using a polynomial symbolic algorithm. We conducted a case study to learn about the challenges that software engineers may face when using GR(1) synthesis for the development of a reactive robotic system. In the case study we developed two variants of a forklift controller, deployed on a Lego robot. The case study employs LTL specification patterns as an extension of the GR(1) specification language, an examination of two specification variants for execution scheduling, traceability from the synthesized controller to constraints in the specification, and generated counter strategies to support understanding reasons for unrealizability. We present the specifications we developed, our observations, and challenges faced during the case study. △ Less

Submitted 2 February, 2016; originally announced February 2016.

Comments: In Proceedings SYNT 2015, arXiv:1602.00786

Journal ref: EPTCS 202, 2016, pp. 58-72

A Manifesto for Semantic Model Differencing

Authors: Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Abstract: Models are heavily used in software engineering and together with their systems they evolve over time. Thus, managing their changes is an important challenge for system maintainability. Existing approaches to model differencing concentrate on heuristics matching between model elements and on finding and presenting differences at a concrete or abstract syntactic level. While showing some success, t… ▽ More Models are heavily used in software engineering and together with their systems they evolve over time. Thus, managing their changes is an important challenge for system maintainability. Existing approaches to model differencing concentrate on heuristics matching between model elements and on finding and presenting differences at a concrete or abstract syntactic level. While showing some success, these approaches are inherently limited to comparing syntactic structures. This paper is a manifesto for research on semantic model differencing. We present our vision to develop semantic diff operators for model comparisons: operators whose input consists of two models and whose output is a set of diff witnesses, instances of one model that are not instances of the other. In particular, if the models are syntactically different but there are no diff witnesses, the models are semantically equivalent. We demonstrate our vision using two concrete diff operators, for class diagrams and for activity diagrams. We motivate the use of semantic diff operators, brie y discuss the algorithms to compute them, list related challenges, and show their application and potential use as new fundamental building blocks for change management in model-driven engineering. △ Less

Submitted 8 September, 2014; originally announced September 2014.

Comments: 10 pages, 7 figures. arXiv admin note: text overlap with arXiv:1409.2355, arXiv:1409.2352

Journal ref: Proceedings Int. Workshop on Models and Evolution (ME'10), co-located with MoDELS'10. J. Dingel and A. Solberg (Eds.): MoDELS Workshops, LNCS 6627, pp. 194 - 203, 2010

An Operational Semantics for Activity Diagrams using SMV

Authors: Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Abstract: This document defines an operational semantics for activity diagrams (ADs) using a translation to SMV. The translation is inspired by the work of Eshuis [Esh06] and extends it with support for data. Each execution step of the SMV module obtained from an AD represents an executed action of this AD with interleaved execution of concurrent branches. An implementation of the given translation was used… ▽ More This document defines an operational semantics for activity diagrams (ADs) using a translation to SMV. The translation is inspired by the work of Eshuis [Esh06] and extends it with support for data. Each execution step of the SMV module obtained from an AD represents an executed action of this AD with interleaved execution of concurrent branches. An implementation of the given translation was used in the context of semantic differencing for ADs [MRR11]. We define the translation and give two examples, showing ADs and their complete representation in SMV. △ Less

Submitted 8 September, 2014; originally announced September 2014.

Comments: 48 pages

CDDiff: Semantic Differencing for Class Diagrams

Authors: Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Abstract: Class diagrams (CDs), which specify classes and the relationships between them, are widely used for modeling the structure of object-oriented systems. As models, programs, and systems evolve over time, during the development lifecycle and beyond it, effective change management is a major challenge in software development, which has attracted much research efforts in recent years. In this paper we… ▽ More Class diagrams (CDs), which specify classes and the relationships between them, are widely used for modeling the structure of object-oriented systems. As models, programs, and systems evolve over time, during the development lifecycle and beyond it, effective change management is a major challenge in software development, which has attracted much research efforts in recent years. In this paper we present cddiff, a semantic diff operator for CDs. Unlike most existing approaches to model comparison, which compare the concrete or the abstract syntax of two given diagrams and output a list of syntactical changes or edit operations, cddiff considers the semantics of the diagrams at hand and outputs a set of diff witnesses, each of which is an object model that is possible in the first CD and is not possible in the second. We motivate the use of cddiff, formally define it, and show how it is computed. The computation is based on a reduction to Alloy. The work is implemented in a prototype Eclipse plug-in. Examples show the unique contribution of our approach to the state-of-the-art in version comparison and evolution analysis. △ Less

Submitted 8 September, 2014; originally announced September 2014.

Comments: 25 pages, 9 figures

Journal ref: Proc. 25th Euro. Conf. on Object Oriented Programming (ECOOP'11), LNCS 6813, pp. 230-254, Springer, 2011

Modal Object Diagrams

Authors: Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Abstract: While object diagrams (ODs) are widely used as a means to document object-oriented systems, they are expressively weak, as they are limited to describe specific possible snapshots of the system at hand. In this paper we introduce modal object diagrams (MODs), which extend the classical OD language with positive/negative and example/invariant modalities. The extended language allows the designer to… ▽ More While object diagrams (ODs) are widely used as a means to document object-oriented systems, they are expressively weak, as they are limited to describe specific possible snapshots of the system at hand. In this paper we introduce modal object diagrams (MODs), which extend the classical OD language with positive/negative and example/invariant modalities. The extended language allows the designer to specify not only positive example models but also negative examples, ones that the system should not allow, positive invariants, ones that all system's snapshots should include, and negative invariants, ones that no system snapshot is allowed to include. Moreover, as a primary application of the extended language we provide a formal verification technique that decides whether a given class diagram satisfies (i.e., models) a multi-modal object diagrams specification. In case of a negative answer, the technique outputs relevant counterexample object models, as applicable. The verification is based on a reduction to Alloy. The ideas are implemented in a prototype Eclipse plug-in. Examples show the usefulness of the extended language in specifying structural requirements of object-oriented systems in an intuitive yet expressive way. △ Less

Submitted 8 September, 2014; originally announced September 2014.

Comments: 25 pages, 9 figures

Journal ref: Proc. 25th Euro. Conf. on Object Oriented Programming (ECOOP'11), LNCS 6813, pp. 281-305, Springer, 2011

ADDiff: Semantic Differencing for Activity Diagrams

Authors: Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Abstract: Activity diagrams (ADs) have recently become widely used in the modeling of workflows, business processes, and web-services, where they serve various purposes, from documentation, requirement definitions, and test case specifications, to simulation and code generation. As models, programs, and systems evolve over time, understanding changes and their impact is an important challenge, which has att… ▽ More Activity diagrams (ADs) have recently become widely used in the modeling of workflows, business processes, and web-services, where they serve various purposes, from documentation, requirement definitions, and test case specifications, to simulation and code generation. As models, programs, and systems evolve over time, understanding changes and their impact is an important challenge, which has attracted much research efforts in recent years. In this paper we present addiff, a semantic differencing operator for ADs. Unlike most existing approaches to model comparison, which compare the concrete or the abstract syntax of two given diagrams and output a list of syntactical changes or edit operations, addiff considers the Semantics of the diagrams at hand and outputs a set of diff witnesses, each of which is an execution trace that is possible in the first AD and is not possible in the second. We motivate the use of addiff, formally define it, and show two algorithms to compute it, a concrete forward-search algorithm and a symbolic xpoint algorithm, implemented using BDDs and integrated into the Eclipse IDE. Empirical results and examples demonstrate the feasibility and unique contribution of addiff to the state-of-the-art in version comparison and evolution analysis. △ Less

Submitted 8 September, 2014; originally announced September 2014.

Comments: 11 pages, 9 figures

Journal ref: Proc. Euro. Soft. Eng. Conf. and SIGSOFT Symp. on the Foundations of Soft. Eng. (ESEC/FSE'11), pp. 179-189, ACM, 2011

CD2Alloy: Class Diagrams Analysis Using Alloy Revisited

Authors: Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Abstract: We present CD2Alloy, a novel, powerful translation of UML class diagrams (CDs) to Alloy. Unlike existing translations, which are based on a shallow embedding strategy, and are thus limited to checking consistency and generating conforming object models of a single CD, and support a limited set of CD language features, CD2Alloy uses a deeper embedding strategy. Rather than mapping each CD construct… ▽ More We present CD2Alloy, a novel, powerful translation of UML class diagrams (CDs) to Alloy. Unlike existing translations, which are based on a shallow embedding strategy, and are thus limited to checking consistency and generating conforming object models of a single CD, and support a limited set of CD language features, CD2Alloy uses a deeper embedding strategy. Rather than mapping each CD construct to a semantically equivalent Alloy construct, CD2Alloy defines (some) CD constructs as new concepts within Alloy. This enables solving several analysis problems that involve more than one CD and could not be solved by earlier works, and supporting an extended list of CD language features. The ideas are implemented in a prototype Eclipse plug-in. The work advances the state-of-the-art in CD analysis, and can also be viewed as an interesting case study for the different possible translations of one modeling language to another, their strengths and weaknesses. △ Less

Submitted 8 September, 2014; originally announced September 2014.

Comments: 15 pages, 8 figures

Journal ref: Model Driven Engineering Languages and Systems (MODELS 2011), Wellington, New Zealand. pp. 592-607, LNCS 6981, 2011

Semantically Configurable Consistency Analysis for Class and Object Diagrams

Authors: Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Abstract: Checking consistency between an object diagram (OD) and a class diagram (CD) is an important analysis problem. However, several variations in the semantics of CDs and ODs, as used in different contexts and for different purposes, create a challenge for analysis tools. To address this challenge in this paper we investigate semantically configurable model analysis. We formalize the variability in th… ▽ More Checking consistency between an object diagram (OD) and a class diagram (CD) is an important analysis problem. However, several variations in the semantics of CDs and ODs, as used in different contexts and for different purposes, create a challenge for analysis tools. To address this challenge in this paper we investigate semantically configurable model analysis. We formalize the variability in the languages semantics using a feature model: each configuration that the model permits induces a different semantics. Moreover, we develop a parametrized analysis that can be instantiated to comply with every legal configuration of the feature model. Thus, the analysis is semantically congured and its results change according to the semantics induced by the selected feature configuration. The ideas are implemented using a parametrized transformation to Alloy. The work can be viewed as a case study example for a formal and automated approach to handling semantic variability in modeling languages. △ Less

Submitted 8 September, 2014; originally announced September 2014.

Comments: 15 pages, 7 figures. Received Best Paper Award and ACM Distinguished Paper Award at the MODELS 2011 Conference

Journal ref: Model Driven Engineering Languages and Systems (MODELS 2011), Wellington, New Zealand. pp. 153-167, LNCS 6981, 2011.

Summarizing Semantic Model Differences

Authors: Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Abstract: Fundamental building blocks for managing and understanding software evolution in the context of model-driven engineering are differencing operators one can use for model comparisons. Semantic model differencing deals with the definition and computation of semantic diff operators for model comparison, operators whose input consists of two models and whose output is a set of diff witnesses, instance… ▽ More Fundamental building blocks for managing and understanding software evolution in the context of model-driven engineering are differencing operators one can use for model comparisons. Semantic model differencing deals with the definition and computation of semantic diff operators for model comparison, operators whose input consists of two models and whose output is a set of diff witnesses, instances of one model that are not instances of the other. However, in many cases the complete set of diff witnesses is too large to be efficiently computed and effectively presented. Moreover, many of the witnesses are very similar and hence not interesting. Thus, an important challenge of semantic differencing relates to witness selection and presentation. In this paper we propose to address this challenge using a summarization technique, based on a notion of equivalence that partitions the set of diff witnesses. The result of the computation is a summary set, consisting of a single representative witness from each equivalence class. We demonstrate our ideas using two concrete diff operators, for class diagrams and for activity diagrams, where the computation of the summary set is efficient and does not require the enumeration of all witnesses. △ Less

Submitted 8 September, 2014; originally announced September 2014.

Comments: 10 pages, 7 figures. ME 2011 - Models and Evolution, Wellington, New Zealand. Ed: B. Schätz, D. Deridder, A. Pierantonio, J. Sprinkle, D. Tamzalit, Wellington, New Zealand, Okt. 2011

An Interim Summary on Semantic Model Differencing

Authors: Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Abstract: This position paper provides an interim summary on the goals and current state of our ongoing research project on semantic model differencing for software evolution. We describe the basics of semantic model differencing, give two examples from our recent work, and discuss future challenges in taking full advantage of the potential of semantic differencing techniques in the context of models' evolu… ▽ More This position paper provides an interim summary on the goals and current state of our ongoing research project on semantic model differencing for software evolution. We describe the basics of semantic model differencing, give two examples from our recent work, and discuss future challenges in taking full advantage of the potential of semantic differencing techniques in the context of models' evolution. △ Less

Submitted 1 September, 2014; originally announced September 2014.

Comments: 3 pages, 5 figures, Softwaretechnik-Trends, Volume 32, Issue 4. November, 2012

Synthesis of Component and Connector Models from Crosscutting Structural Views

Authors: Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Abstract: We present component and connector (C&C) views, which specify structural properties of component and connector models in an expressive and intuitive way. C&C views provide means to abstract away direct hierarchy, direct connectivity, port names and types, and thus can crosscut the traditional boundaries of the implementation-oriented hierarchical decomposition of systems and sub-systems, and refle… ▽ More We present component and connector (C&C) views, which specify structural properties of component and connector models in an expressive and intuitive way. C&C views provide means to abstract away direct hierarchy, direct connectivity, port names and types, and thus can crosscut the traditional boundaries of the implementation-oriented hierarchical decomposition of systems and sub-systems, and reflect the partial knowledge available to different stakeholders involved in a system's design. As a primary application for C&C views we investigate the synthesis problem: given a C&C views specification, consisting of mandatory, alternative, and negative views, construct a concrete satisfying C&C model, if one exists. We show that the problem is NP-hard and solve it, in a bounded scope, using a reduction to SAT, via Alloy. We further extend the basic problem with support for library components, specification patterns, and architectural styles. The result of synthesis can be used for further exploration, simulation, and refinement of the C&C model or, as the complete, final model itself, for direct code generation. A prototype tool and an evaluation over four example systems with multiple specifications show promising results and suggest interesting future research directions towards a comprehensive development environment for the structure of component and connector designs. △ Less

Submitted 25 August, 2014; originally announced August 2014.

Comments: 11 pages, 10 figures

Journal ref: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE'13), Eds.: B. Meyer, L. Baresi, M. Mezini, pages 444-454, ACM New York, 2013

Verifying Component and Connector Models against Crosscutting Structural Views

Authors: Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Abstract: The structure of component and connector (C&C) models, which are used in many application domains of software engineering, consists of components at different containment levels, their typed input and output ports, and the connectors between them. C&C views, presented in [24], can be used to specify structural properties of C&C models in an expressive and intuitive way. In this work we address the… ▽ More The structure of component and connector (C&C) models, which are used in many application domains of software engineering, consists of components at different containment levels, their typed input and output ports, and the connectors between them. C&C views, presented in [24], can be used to specify structural properties of C&C models in an expressive and intuitive way. In this work we address the verification of a C&C model against a C&C view and present efficient (polynomial) algorithms to decide satisfaction. A unique feature of our work, not present in existing approaches to checking structural properties of C&C models, is the generation of witnesses for satisfaction/non-satisfaction and of short naturallanguage texts, which serve to explain and formally justify the verification results and point the engineer to its causes. A prototype tool and an evaluation over four example systems with multiple views, performance and scalability experiments, as well as a user study of the usefulness of the witnesses for engineers, demonstrate the contribution of our work to the state-of-the-art in component and connector modeling and analysis. △ Less

Submitted 27 June, 2014; originally announced June 2014.

Comments: 11 pages, 8 figures

Journal ref: 36th International Conference on Software Engineering (ICSE 2014). Pages 95-105. Hyderabad, India, ACM New York, June 2014