#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.
#OnlineFirst
Automated and logically exhaustive generation of traffic scenarios at road junctions using a multi-level danger definition
Aren A. Babikian, Attila Ficsor, Oszkár Semeráth, Gunter Mussbacher & Dániel Varró
doi.org/10.1007/s102...doi.org/10.1007/s10270... #OnlineFirst
Formal modelling and verifying eIDAS multi-factor authentication with interface-based threat analysis
Matteo Paier, Roberto L. G. Van Eeden & Marino Miculan
doi.org/10.1007/s102...Formal modelling and verifying... 
Formal modelling and verifying eIDAS multi-factor authentication with interface-based threat analysis - Software and Systems Modeling
This paper introduces a methodology for the formal modelling and verification of multi-factor authentication (MFA) schemes utilized in eIDAS digital identity cards. Our approach employs an interface-based threat model to systematically analyse potential vulnerabilities and enumerate a range of threat scenarios based on varying attacker capabilities. We demonstrate the automated generation of ProVerif models for these scenarios using the Italian Carta di Identità Elettronica (CIE), an eIDAS-compliant digital identity card, as a practical case study. Our analysis reveals several security weaknesses; notably, an attacker possessing only Level 1 (i.e. single-factor) credentials can, in certain circumstances, achieve Level 2 multi-factor authentication without needing to compromise any communication interface. To mitigate these vulnerabilities, we propose minor modifications to the protocols. Furthermore, at Level 3, our analysis shows that the authentication scheme relying on the CieID smartphone application presents a broader attack surface compared to the method employing a PC with a smart card reader. The interface-based modelling and analysis methodology presented in this work offers a valuable framework that can be adapted for the security assessment of other eIDAS digital identity cards.
#OnlineFirst
Mu-FRET: a catalogue and tool for requirement refactoring
Matt Luckcuck, Oisín Sheridan, Marie Farrell & Rosemary Monahan
doi.org/10.1007/s102...Mu-FRET: a catalogue and tool ... 
Mu-FRET: a catalogue and tool for requirement refactoring - Software and Systems Modeling
In this paper, we present a catalogue of refactorings for formalised requirements, which improve the structure of requirements without changing their behaviour. As a requirements set evolves and grows in complexity, refactoring is needed to improve clarity, eliminate repetition, and restructure requirements without introducing errors. We integrate our approach with the formal requirement language fretish, and we implement the approach in our Mu-FRET tool. Our approach provides a rigorous grounding for refactoring formalised requirements with guarantees of semantic preservation between requirements before and after refactoring. To this end, Mu-FRET uses the Metric Temporal Logic (MTL) semantics that underpins fretish requirements to formally verify that refactoring has preserved the underlying meaning of the requirements; which is not possible for natural-language requirements. We demonstrate and evaluate our contributions on a range of complex and industry-scale use cases from safety–critical domains including aerospace and medical devices.
#OnlineFirst
Integrating SysML and AUTOSAR: model transformation in automotive MBSE
Faezeh Siavashi, Horacio Hoyos Rodriguez, Vera Pantelic, Monika Jaskolka, Alessandro Verde, Mark Lawford & Richard Paige
doi.org/10.1007/s102...Integrating SysML and AUTOSAR:... #OnlineFirst
Model-based digital twin engineering: insights, challenges, and future directions
Philipp Zech, Souvik Barat, Benjamin Nast, Bentley Oakes, Judith Michael, Steffen Zschaler, Balbir Barn & Ruth Breu
doi.org/10.1007/s102...Model-based digital twin engin... Model-based digital twin engineering: insights, challenges, and future directions | Software and Systems Modeling | Springer Nature Link
Model-based engineering (MBE) is a powerful paradigm that leverages models as essential pillars of the development process, enabling teams to clarify requi
#OnlineFirst
SMOKE2.0 whitebox anonymization of sensitive information in Simulink with structure preservation
Alexander Boll, Manuel Ohrndorf & Timo Kehrer
doi.org/10.1007/s102...SMOKE2.0 whitebox anonymizatio... 
SMOKE2.0 whitebox anonymization of sensitive information in Simulink with structure preservation - Software and Systems Modeling
Simulink is widely used across various industries to model and simulate cyber-physical systems. Most industry-built models contain sensitive information, which prevents companies from sharing models with interested third parties, such as researchers or collaborating companies. However, advancing model-based engineering research requires access to such models—either to derive empirical insights or to evaluate new tools. While initiatives to replace industry-built models with open-source alternatives exist, they offer only a limited remedy. In this work, we present a novel approach with Smoke, a Simulink anonymization tool designed to selectively remove sensitive information within models. This allows companies to share relevant parts of their models with researchers or other third parties while safeguarding all sensitive information. Smoke’s whitebox design preserves the model’s original format and structure, ensuring that meaningful insights remain accessible. We evaluated the tool on an extensive set of open-source models and found it successfully removes sensitive information, while preserving model structure. A video demonstration of Smoke is available online at https://youtu.be/0i42BzgJAUA .
#OnlineFirst
Unlocking the power of environment assumptions for unit proofs
Siddharth Priya, Temesghen Kahsai & Arie Gurfinkel
doi.org/10.1007/s102...Unlocking the power of environ... #OnlineFirst
A conversational tool for AI-driven feedback for UML modeling
Pasquale Ardimento, Mario Luca Bernardi, Marta Cimitile & Michele Scalera
doi.org/10.1007/s102...A conversational tool for AI-d... 
A conversational tool for AI-driven feedback for UML modeling - Software and Systems Modeling
Teaching the unified modeling language (UML) is a critical task that can benefit from emerging artificial intelligence-based solutions. This paper presents UML Miner, a visual paradigm plugin designed to support the teaching and learning of UML by capturing and analyzing students’ modeling activities to deliver personalized, context-aware feedback. The tool records fine-grained software modeling actions, storing them in an event log. For each diagram, a natural language description and its XML representation are stored separately. Modeling behavior is reconstructed through process mining techniques and compared with a reference model created by the instructor using conformance checking. This analysis adopts a declarative approach, leveraging the declare language to specify behavioral constraints without enforcing a rigid action sequence, thereby accommodating multiple valid modeling strategies while preserving semantic rigor. The detected violations, together with the diagram’s natural language and XML representations, are integrated into a retrieval-augmented generation-enabled large language model, which combines accumulated knowledge with the discovered process constraints to generate enriched, pedagogically meaningful feedback in real time. An exploratory case study conducted in a real-world learning scenario evaluates the tool’s performance from both qualitative and quantitative perspectives, demonstrating its potential to improve learning outcomes and student engagement.
#OnlineFirst
Model-based software sustainability analysis and improvement
Kevin Lano, Zishan Rahman & Lyan Alwakeel
doi.org/10.1007/s102...Model-based software sustainab... 
Model-based software sustainability analysis and improvement - Software and Systems Modeling
The environmental sustainability of software has become a significant issue for the use of computing technologies. The pervasive use of software applications throughout society has potential negative environmental impacts due to the energy used by software execution, and the resulting greenhouse gas (GHG) emissions. In this paper, we describe techniques for the identification of software energy use flaws at the software modelling level, and we define techniques for the removal of such flaws via refactoring or the use of alternative specification/design modelling elements. The key idea is that energy use flaws are corrected once at the software modelling level, in order to obtain energy-efficient benefits across all target platforms. We provide a detailed evaluation to show that the proposed improvements do result in reduced energy use across multiple implementation languages and platforms. The outcome represents a novel approach for software sustainability using software models, incorporated into an established toolset for model-driven engineering.
SoSyM