#OnlineFirstA theory of composable modeling language components
Jérôme Pfeiffer & Andreas Wortmann
doi.org/10.1007/s102...A theory of composable modelin... 
A theory of composable modeling language components - Software and Systems Modeling
Modern-day software has become increasingly complex and ubiquitous in many domains. In many cases, the scarcity of software engineering experts means that domain experts must engage in software development tasks. (DSLs) can help bridge this gap by enabling domain experts to express solutions in familiar domain terms. Engineering such (DSLs) is complex. This complexity arises from the variety of artifacts involved—such as grammars, well-formedness rules, and code generators—and from the need to integrate these artifacts across languages. In software language engineering, language workbenches for textual, external modeling languages with translational semantics seem to be a popular, which includes inhabitants such as Xtext, Neverlang, MontiCore, and Spoofax. Yet, reusing existing languages in these environments is often piecemeal and driven by the constraints of specific realization technologies (e.g., Xtend, FreeMarker). This typically requires software language engineers to create DSLs for domain experts, rather than enabling domain experts to reuse and adapt languages themselves. As a result, enabling the systematic reuse of software languages remains a fundamental challenge in software engineering. To reduce the gap between problem domain expertise and software language engineering solution expertise, we have conceived a top-down software language reuse method that enables domain experts to reuse existing languages through formally specified language components that encapsulate the realizations of syntax and semantics of (a fragment of) a language packed ready for systematic reuse. To ease its understanding of our method and its adoption to other technological spaces, we describe our methods and the composition process independent of specific technologies. The presented method of language reuse aims to advance software language engineering for textual, external, translational (DSLs) and may serve as the basis for further investigation of formalizing language reuse.
#OnlineFirstExecution-time opacity control for timed automata
Étienne André, Marie Duflot, Laetitia Laversa & Engel Lefaucheux
doi.org/10.1007/s102...Execution-time opacity control... #OnlineFirstDeductive reasoning about embedded systems using reachable abstract states invariants
Philip Tasche, Paula Herber & Marieke Huisman
doi.org/10.1007/s102...Deductive reasoning about embe... 
Deductive reasoning about embedded systems using reachable abstract states invariants - Software and Systems Modeling
Deductive verification is often more efficient than alternative techniques like model checking at reasoning about functional properties of programs. This is especially true when the program under verification contains very large or unbounded data ranges that model checkers struggle with. However, modular deductive verifiers struggle with verifying global properties, which are often crucial in concurrent and reactive embedded systems. Embedded systems often require complex user-defined invariants to capture the global state for the verification of local annotations, demanding high effort and expertise from the user. In this paper, we propose a method to automatically generate compact invariants that are sufficiently strong to enable effective deductive verification of global properties in embedded systems. Our key idea is that a good level of abstraction can be found automatically by choosing variables for refinement that influence relevant events and process interactions. We use this idea together with abstract interpretation to build a system’s state space, abstracted to the relevant part for a given global property. We demonstrate the effectiveness of our approach on a SystemC design of an automotive control system that has in the past proved challenging to verify.
#OnlineFirst
REST in pieces: a controlled experiment to dissect the effects of a domain-specific language for code to cloud API migration
Maximilian Schiedermeier, Bettina Kemme & Jörg Kienzle
doi.org/10.1007/s102...
REST in pieces: a controlled e...
REST in pieces: a controlled experiment to dissect the effects of a domain-specific language for code to cloud API migration - Software and Systems Modeling
Domain-specific languages (DSLs) are an efficient means to counter accidental complexity and are therefore a key technology for model-driven engineering (MDE). Despite the potential of DSLs, there is a lack of empirical research on the practical effects and developer perception of DSL-driven tools. In this paper, we present a controlled experiment with 28 participants around a previously developed DSL- and MDE-based toolchain, which assists the migration of legacy software to REST. We compare the developer performance for (a) “DSL+MDE toolchain" and (b) “classic manual software migration" analysing and quantifying the effects of the DSL, as well as the perception of the DSL by the developers. In certain cases, we measured a significant correlation between toolchain use and performance gains for developers. Detailed analysis of developer activities suggests that the DSL toolchain alleviates tasks which are error-prone or time-consuming in the manual alternative. We then extracted acceptance-hindering factors from the feedback of the participants and derived a series of recommendations for MDE practitioners who seek to develop DSL-based tools.
#OnlineFirst
A conceptual framework and city metaphor for investigating the interaction of developers with software artifacts
Thierry Sorg, Amine Abbad-Andaloussi, Jonas Länzlinger, Ekkart Kindler & Barbara Weber
doi.org/10.1007/s102...A conceptual framework and cit... #OnlineFirst
Reactive synthesis specification review for validity and quality
Shahar Maoz, Rafi Shalom & Ophir Taieb
doi.org/10.1007/s102...Reactive synthesis specificati... Reactive synthesis specification review for validity and quality - Software and Systems Modeling
Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. While the synthesized system is guaranteed to be correct w.r.t. the specification, the specification itself may not reflect the intended requirements and hence requires validation. Beyond validity, the specification may have quality issues that may impair its readability and maintainability. In this work, we adapt ideas from software engineering and formal verification to present new methods for the validation and the detection of quality issues in reactive system specifications for synthesis. Our first contribution provides a method for specification validation based on a systematic exploration of the specification elements. Specifically, we present algorithms to generate a small scenario suite that demonstrates the meaning of each element in the specification in the context of the behaviors of a controller that is synthesized from it. Our second and third contributions provide means for the detection of quality issues in the specification. Specifically, we present algorithms to detect unnecessary variables that appear in specification elements as well as to detect fine-grained syntactic and semantic specification clones and suggest corresponding refactoring. An important characteristic of our work is that both the algorithms and the controller representation are symbolic. This allows our work to scale well to specifications over large state spaces. We have implemented our ideas in the Spectra synthesis environment and evaluated performance and effectiveness over benchmarks from the literature.
#OnlineFirst
Evaluation of modeling methods for systems analysis and development (EMMSAD): past, present, and artificial intelligence eras
Yingying Zhang, Keng Siau & Joseph Sung
doi.org/10.1007/s102...Evaluation of modeling methods... #OnlineFirst
Engineering a cognition-based specification method
Robert Deckers & Patricia Lago
doi.org/10.1007/s102...Engineering a cognition-based ... 
Engineering a cognition-based specification method - Software and Systems Modeling
Context Software development is inherently a human cognitive task that involves the capture and integration of diverse knowledge and decisions from multiple stakeholders. Existing specification methods and languages mostly rely on computer-based or mathematical primitives, leading to a disconnect between how people naturally think and communicate, and how systems are specified. Therefore, we are investigating a method, called MuDForM (Multi-Domain Formalization Method), to formalize and integrate the knowledge of multiple domains into domain models and into specifications in terms of those domain models. We created a first coherent definition of the method, which emerged from several case study evaluations published in previous works. Goal Establish a method definition that is explicitly based on concepts from human cognition. Method We studied literature in (language) philosophy, linguistics, and cognitive science, to identify concepts that can serve as the cognitive underpinning of the method’s metamodel. We made a model of those concepts and connected them to MuDForM’s metamodel via an explicit method definition structure and analyzed the result. Result The paper defines the conceptual and structural groundwork for illustrating how a specification method can be constructed based on insights into human cognition and communication. It provides a coherent model of cognitive specification aspects, which grounds the modeling concepts in MuDForM ’s metamodel and makes it cognition-based. We also identified additional cognitive aspects that call for future work and the possible extension of the metamodel. The paper clarifies MuDForM ’s objective to support the transformation of natural language into unambiguous, cognition-aligned models.
#OnlineFirst
Failure behavior modeling via atomic modeling concepts
Stefan Kaalen, Mattias Nyberg & Adrian Westerberg
doi.org/10.1007/s102...Failure behavior modeling via ... 
Failure behavior modeling via atomic modeling concepts - Software and Systems Modeling
It is essential to thoroughly analyze the probability of a system failure of safety-critical systems before release. Since this is typically unfeasible through testing alone, probabilistic safety analysis of models is commonly used. However, many modeling languages are lacking in either expressiveness or the ability to reflect the system architecture. The results of these weaknesses are models that are inaccurate in terms of either their behavior or architecture with respect to the system being analyzed. The few languages that overcome both these hurdles are instead overly complicated, resulting in models that are difficult to understand and prone to unintentional errors. To overcome this issue, the modeling language PAFML (Pattern Assisted Failure Modeling Language) is here presented which, while being expressive and able to reflect the system architecture, still satisfies a high level of simplicity. PAFML models are analyzed through transformation to SSF (Stochastic StateFlow), a preexisting language for analysis of stochastic models. PAFML is evaluated both through an interview study with industry professionals in systems safety and through modeling several industrial systems and modeling patterns common in failure behavior models.
#OnlineFirst
Formalizing smart contract design patterns with DCR graphs
Mojtaba Eshghie, Wolfgang Ahrendt, Cyrille Artho, Thomas Troels Hildebrandt & Gerardo Schneider
doi.org/10.1007/s102...Formalizing smart contract des... 
Formalizing smart contract design patterns with DCR graphs - Software and Systems Modeling
Smart contracts manage blockchain assets and embody business processes. Yet, mainstream languages lack explicit support for process concepts such as roles, action dependencies, and time constraints, leading to increased implementation complexity and analysis challenges. To address this, we use Dynamic Condition Response (DCR) graphs, a formal business process modeling language, to formalize the semantics of smart contract business logic. Modeling smart contracts in DCR graphs involves translating their underlying behavioral logic into a declarative visual model using DCR’s explicit constructs for events, roles, data, time, and inter-event relationships. Furthermore, we systematically model 15 common high-level smart contract design patterns, representing recurring solutions to business logic-level problems. These formalizations reduce ambiguity compared to informal descriptions and serve as language-independent specifications. We demonstrate the modeling process through three complete smart contract case studies that combine six design patterns. Our modeling methodology, formalizations, and correspondence between smart contract semantics and DCR graphs enable future automated analysis and verification.
SoSyM