2026
Book
Open Access
Preface to Journeys between formal methods and the railway industry. Essays dedicated to Alessandro Fantechi on the occasion of his 70th birthday
Ter Beek Maurice Henri, Gnesi Stefania, Haxthausen Anne E., Semini Laura
This Festschrift contains 18 contributions by collaborators, colleagues and friends of Alessandro Fantechi to celebrate his 70th birthday.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. i-xvi
DOI: 10.1007/978-3-032-12484-5
Project(s): Sustainable Mobility National Research Center
Metrics:
Ter Beek Maurice Henri, Gnesi Stefania, Haxthausen Anne E., Semini Laura
This Festschrift contains 18 contributions by collaborators, colleagues and friends of Alessandro Fantechi to celebrate his 70th birthday.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. i-xvi
DOI: 10.1007/978-3-032-12484-5
Project(s): Sustainable Mobility National Research Center
Metrics:
See at:
CNR IRIS 
| link.springer.com | CNR IRIS 
2026
Contribution to book
Open Access
Towards dynamic classification in domain modeling with Jjodel
Ter Beek Maurice Henri, Bucchiarone Antonio, Pierantonio Alfonso, Selic Bran
This work addresses the limitations of traditional object-oriented classification in representing evolving systems. Conventional classification enforces rigid hierarchies that hinder dynamic reclassification, concurrent viewpoints, and transient or overlapping states, thus limiting their usefulness for systems that exhibit change, context sensitivity, or adaptation. We propose a modeling notation that extends UML class diagrams with declarative behavioral dynamics directly embedded in structural information. Unlike approaches that separate structure and behavior, our notation unifies them in a framework suitable for both conceptual/domain modeling and evolutionary, context-aware dynamics. The notation is fully defined, including abstract syntax, diagrammatic syntax, semantics, and simulation, within the Jjodel platform, ensuring rigor and tool support. Its structural nature enables the declarative specification of dynamics without imperative constructs. Moreover, the notation can be connected to frameworks for formal verification and model checking, enabling analysis of dynamic properties. Applicability is illustrated through a context-aware scenario in which enriched structural models can be simulated, reasoned about, and eventually verified.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. 193-215
DOI: 10.1007/978-3-032-12484-5_11
Metrics:
Ter Beek Maurice Henri, Bucchiarone Antonio, Pierantonio Alfonso, Selic Bran
This work addresses the limitations of traditional object-oriented classification in representing evolving systems. Conventional classification enforces rigid hierarchies that hinder dynamic reclassification, concurrent viewpoints, and transient or overlapping states, thus limiting their usefulness for systems that exhibit change, context sensitivity, or adaptation. We propose a modeling notation that extends UML class diagrams with declarative behavioral dynamics directly embedded in structural information. Unlike approaches that separate structure and behavior, our notation unifies them in a framework suitable for both conceptual/domain modeling and evolutionary, context-aware dynamics. The notation is fully defined, including abstract syntax, diagrammatic syntax, semantics, and simulation, within the Jjodel platform, ensuring rigor and tool support. Its structural nature enables the declarative specification of dynamics without imperative constructs. Moreover, the notation can be connected to frameworks for formal verification and model checking, enabling analysis of dynamic properties. Applicability is illustrated through a context-aware scenario in which enriched structural models can be simulated, reasoned about, and eventually verified.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. 193-215
DOI: 10.1007/978-3-032-12484-5_11
Metrics:
See at:
CNR IRIS | link.springer.com | CNR IRIS | CNR IRIS
2026
Journal article
Open Access
Editorial introducing the new editors-in-chief
Ter Beek Maurice Henri, Johnsen Einar Broch
Editorial Introducing the New Editors-in-ChiefSource: FORMAL ASPECTS OF COMPUTING, vol. 38 (issue 1), pp. 1-2
DOI: 10.1145/3787980
Metrics:
Ter Beek Maurice Henri, Johnsen Einar Broch
Editorial Introducing the New Editors-in-ChiefSource: FORMAL ASPECTS OF COMPUTING, vol. 38 (issue 1), pp. 1-2
DOI: 10.1145/3787980
Metrics:
See at:
dl.acm.org | CNR IRIS | CNR IRIS
2026
Journal article
Open Access
Large language models as design partners: automating graphical mockups to refine requirements
Broccia Giovanna, Ter Beek Maurice Henri, Ferrari Alessio
Can large language models help designers move faster without sacrificing human centrality? Researchers from CNR–ISTI and University College Dublin are exploring how large language models can support the rapid creation and refinement of industrial graphical user interfaces through a case study involving the Italian railway operator Trenord, helping development teams move more quickly from textual requirements to interactive mockups, while keeping humans at the centre of the design process.Source: ERCIM NEWS, vol. 145, pp. 37-38
Project(s): CN MOST (National Sustainable Mobility Centre) Spoke 4: Rail Transportation
Broccia Giovanna, Ter Beek Maurice Henri, Ferrari Alessio
Can large language models help designers move faster without sacrificing human centrality? Researchers from CNR–ISTI and University College Dublin are exploring how large language models can support the rapid creation and refinement of industrial graphical user interfaces through a case study involving the Italian railway operator Trenord, helping development teams move more quickly from textual requirements to interactive mockups, while keeping humans at the centre of the design process.Source: ERCIM NEWS, vol. 145, pp. 37-38
Project(s): CN MOST (National Sustainable Mobility Centre) Spoke 4: Rail Transportation
See at:
ercim-news.ercim.eu | CNR IRIS | CNR IRIS
2026
Book
Open Access
Preface to the Proceedings of the 7th workshop on models for formal analysis of real systems (MARS'26)
Ter Beek Maurice Henri, Gössler Gregor
These proceedings contain the papers that were presented at the 7th Workshop on Models for Formal Analysis of Real Systems (MARS 2026), which took place on 12 April 2026 in Turin, Italy, as a satellite event of the 29th International Joint Conferences on Theory and Practice of Software (ETAPS 2026). The goal of MARS is to bring together researchers from different communities who are developing formal models of real systems in areas where complex models occur (e.g., networks, cyber-physical systems, hardware/software codesign, biology). The motivation for MARS stems from the following two observations: - Large case studies are essential to show that specification formalisms and modelling techniques are applicable to real systems, whereas many papers only consider toy examples or tiny case studies. - Developing an accurate model of a real system takes a large amount of time, often months or years. In most papers, however, salient details of the model need to be skipped due to lack of space, and to leave room for formal verification methodologies and results. MARS aims at remedying these issues, emphasising modelling over verification, so as to retain lessons learned from formal modelling, which are not usually discussed elsewhere, and which may lay the basis for future analysis and comparison.Source: ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, vol. 443, pp. iii-iv
DOI: 10.4204/eptcs.443
Metrics:
Ter Beek Maurice Henri, Gössler Gregor
These proceedings contain the papers that were presented at the 7th Workshop on Models for Formal Analysis of Real Systems (MARS 2026), which took place on 12 April 2026 in Turin, Italy, as a satellite event of the 29th International Joint Conferences on Theory and Practice of Software (ETAPS 2026). The goal of MARS is to bring together researchers from different communities who are developing formal models of real systems in areas where complex models occur (e.g., networks, cyber-physical systems, hardware/software codesign, biology). The motivation for MARS stems from the following two observations: - Large case studies are essential to show that specification formalisms and modelling techniques are applicable to real systems, whereas many papers only consider toy examples or tiny case studies. - Developing an accurate model of a real system takes a large amount of time, often months or years. In most papers, however, salient details of the model need to be skipped due to lack of space, and to leave room for formal verification methodologies and results. MARS aims at remedying these issues, emphasising modelling over verification, so as to retain lessons learned from formal modelling, which are not usually discussed elsewhere, and which may lay the basis for future analysis and comparison.Source: ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, vol. 443, pp. iii-iv
DOI: 10.4204/eptcs.443
Metrics:
See at:
cgi.cse.unsw.edu.au | CNR IRIS | CNR IRIS
2026
Journal article
Open Access
Tony Hoare: In memoriam
Ter Beek Maurice H., Johnsen Einar Broch
Editorial commemorating Tony Hoare and introducing Krzysztof Apt’s obituary for Tony Hoare.Source: FORMAL ASPECTS OF COMPUTING, vol. 38 (issue 2), p. 1
DOI: 10.1145/3816421
Metrics:
Ter Beek Maurice H., Johnsen Einar Broch
Editorial commemorating Tony Hoare and introducing Krzysztof Apt’s obituary for Tony Hoare.Source: FORMAL ASPECTS OF COMPUTING, vol. 38 (issue 2), p. 1
DOI: 10.1145/3816421
Metrics:
See at:
dl.acm.org | CNR IRIS | CNR IRIS
2026
Contribution to book
Open Access
Formal methods for railway systems: a survey of research and technology transfer projects
Basile Davide, Ter Beek Maurice Henri, Broccia Giovanna, Gnesi Stefania, Mazzanti Franco, Spagnolo Giorgio Oronzo, Bacherini Stefano, Becheri Carlo, Grasso Daniele, Magnani Gianluca, Tempestini Matteo, Zingoni Niccolò, Ferrari Alessio
This paper offers a retrospective on collaborative projects that involved Alessandro Fantechi and the authors over the past two decades, from the shared perspective of the Formal Methods and Tools (FMT) lab of the Italian National Research Council (CNR) and former collaborators at General Electric (GE) Transportation and Alstom. The focus is on research and technology transfer efforts in the field of formal methods for railway systems, where Alessandro Fantechi’s contributions have been central to the development and application of formal specification, model-based verification, and tool-supported analysis. Joint work in projects such as ASTRail, 4SECURail, and TRACE-IT, as well as in industrial collaborations with Alstom and GE Transportation Systems illustrates the sustained impact of these activities on both academic research and industrial practice. This contribution reflects on the evolution of these efforts, the formal methods adopted, and the outcomes achieved in terms of methodologies, tools, and integration into safety-critical development processes. It also highlights the collaborative environment fostered across institutions and organizations, which has been instrumental in advancing the use of formal methods in the railway domain.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. 31-54
DOI: 10.1007/978-3-032-12484-5_3
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
Basile Davide, Ter Beek Maurice Henri, Broccia Giovanna, Gnesi Stefania, Mazzanti Franco, Spagnolo Giorgio Oronzo, Bacherini Stefano, Becheri Carlo, Grasso Daniele, Magnani Gianluca, Tempestini Matteo, Zingoni Niccolò, Ferrari Alessio
This paper offers a retrospective on collaborative projects that involved Alessandro Fantechi and the authors over the past two decades, from the shared perspective of the Formal Methods and Tools (FMT) lab of the Italian National Research Council (CNR) and former collaborators at General Electric (GE) Transportation and Alstom. The focus is on research and technology transfer efforts in the field of formal methods for railway systems, where Alessandro Fantechi’s contributions have been central to the development and application of formal specification, model-based verification, and tool-supported analysis. Joint work in projects such as ASTRail, 4SECURail, and TRACE-IT, as well as in industrial collaborations with Alstom and GE Transportation Systems illustrates the sustained impact of these activities on both academic research and industrial practice. This contribution reflects on the evolution of these efforts, the formal methods adopted, and the outcomes achieved in terms of methodologies, tools, and integration into safety-critical development processes. It also highlights the collaborative environment fostered across institutions and organizations, which has been instrumental in advancing the use of formal methods in the railway domain.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. 31-54
DOI: 10.1007/978-3-032-12484-5_3
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
See at:
CNR IRIS | link.springer.com | CNR IRIS | CNR IRIS
2026
Journal article
Open Access
A history of formal methods in railways
Ter Beek Maurice, Fantechi Alessandro, Ferrari Alessio, Gnesi Stefania, Haxthausen Anne E., Lecomte Thierry
The engineering of industrial systems, particularly in safety-critical domains such as railways, demands rigorous verification and validation processes to ensure system dependability. Formal methods have emerged as powerful tools to complement traditional software engineering practices. In the railway sector, which increasingly relies on complex, distributed, and cyber-physical control systems, formal methods have demonstrated particular value for many decades now. In this paper, we provide a retrospective overview of the application of formal methods and tools in the railway domain, with emphasis on two prominent verification approaches and one frequently verified railway system: modeling and validation with the B method and tools and formal verification of interlocking systems by model checking. We explore their role in the design and development of key railway systems, highlighting both academic research and industrial success stories, as witnessed by international projects and initiatives. We conclude with an outlook on the potential of integrating AI and formal methods to enhance the efficiency of next-generation railway systems.Source: FORMAL ASPECTS OF COMPUTING
DOI: 10.1145/3802545
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
Ter Beek Maurice, Fantechi Alessandro, Ferrari Alessio, Gnesi Stefania, Haxthausen Anne E., Lecomte Thierry
The engineering of industrial systems, particularly in safety-critical domains such as railways, demands rigorous verification and validation processes to ensure system dependability. Formal methods have emerged as powerful tools to complement traditional software engineering practices. In the railway sector, which increasingly relies on complex, distributed, and cyber-physical control systems, formal methods have demonstrated particular value for many decades now. In this paper, we provide a retrospective overview of the application of formal methods and tools in the railway domain, with emphasis on two prominent verification approaches and one frequently verified railway system: modeling and validation with the B method and tools and formal verification of interlocking systems by model checking. We explore their role in the design and development of key railway systems, highlighting both academic research and industrial success stories, as witnessed by international projects and initiatives. We conclude with an outlook on the potential of integrating AI and formal methods to enhance the efficiency of next-generation railway systems.Source: FORMAL ASPECTS OF COMPUTING
DOI: 10.1145/3802545
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
See at:
dl.acm.org | CNR IRIS | CNR IRIS
2026
Other
Restricted
Report on the results achieved by the project in the application of the proposed modeling and evaluation methods to the considered case studies
Basile Davide, Ter Beek Maurice, Carnevali Laura, Chiaradonna Silvano, Di Giandomenico Felicita, Fantechi Alessandro, Gori Gloria, Zecchi Jacopo
ADVENTURE (ADVancEd iNtegraTed evalUation of Railway systEms) aims at developing innovative solutions for the evaluation of complex railway systems. Using Model-Driven Engineering (MDE) methods and multi-paradigm or multi-formalism approaches to help create bridges between different abstraction levels, the project focuses on the following objectives: 1) qualitative evaluation of safety of complex distributed railway systems, by means of diverse techniques such as compositional model checking, synthesis of specifications given as behavioral interfaces, and tool support for relating specifications with implementations; 2) quantitative evaluation of dependability attributes in spite of failures, in particular considering communication failures, through quantitative modeling and evaluation of the timed failure logic of the system; 3) quantitative evaluation of trade-offs between energy efficiency and availability/performance, considering different smart policies for energy savings and taking into account failures, criticalities, and priorities of the system under analysis. The developed solutions have been experimented and validated by their application to different case studies, that are considered as representative of the innovation trends in railways, namely decentralized interlocking systems, standard interfaces and smart deicing systems. This deliverable reports the results of the application of the techniques that have been identified in the previous work [1] to the case studies. Specifically, Chapter 2 discusses the application of compositional methods for interlocking verification and the application of interfaces for testing the adequacy of the abstraction level; Chapter 3 addresses the application of methods for the quantitative evaluation of dependability to railway case studies; and Chapter 4 illustrates the application of methods for the quantitative evaluation of trade-offs between dependability properties and energy consumption to railway switch heater anti-icing systems.Project(s): ADVancEd iNtegraTed evalUation of Railway systEms
Basile Davide, Ter Beek Maurice, Carnevali Laura, Chiaradonna Silvano, Di Giandomenico Felicita, Fantechi Alessandro, Gori Gloria, Zecchi Jacopo
ADVENTURE (ADVancEd iNtegraTed evalUation of Railway systEms) aims at developing innovative solutions for the evaluation of complex railway systems. Using Model-Driven Engineering (MDE) methods and multi-paradigm or multi-formalism approaches to help create bridges between different abstraction levels, the project focuses on the following objectives: 1) qualitative evaluation of safety of complex distributed railway systems, by means of diverse techniques such as compositional model checking, synthesis of specifications given as behavioral interfaces, and tool support for relating specifications with implementations; 2) quantitative evaluation of dependability attributes in spite of failures, in particular considering communication failures, through quantitative modeling and evaluation of the timed failure logic of the system; 3) quantitative evaluation of trade-offs between energy efficiency and availability/performance, considering different smart policies for energy savings and taking into account failures, criticalities, and priorities of the system under analysis. The developed solutions have been experimented and validated by their application to different case studies, that are considered as representative of the innovation trends in railways, namely decentralized interlocking systems, standard interfaces and smart deicing systems. This deliverable reports the results of the application of the techniques that have been identified in the previous work [1] to the case studies. Specifically, Chapter 2 discusses the application of compositional methods for interlocking verification and the application of interfaces for testing the adequacy of the abstraction level; Chapter 3 addresses the application of methods for the quantitative evaluation of dependability to railway case studies; and Chapter 4 illustrates the application of methods for the quantitative evaluation of trade-offs between dependability properties and energy consumption to railway switch heater anti-icing systems.Project(s): ADVancEd iNtegraTed evalUation of Railway systEms
2026
Conference article
Open Access
Asynchronous team automata
Basile Davide, Ter Beek Maurice H., Proença José
Team automata were introduced as a flexible extension of I/O automata to model collaborative behaviour in component-based and distributed systems. Their distinctive features include multi-party communication and a liberal synchronisation mechanism: components may jointly execute shared actions according to synchronisation policies that specify which subsets of components participate as senders or receivers. While this makes team automata well suited for modelling coordination, existing communication is synchronous and therefore insufficient for capturing certain behavioural aspects (e.g., due to message reordering) of modern networks and distributed systems, in which communication is typically asynchronous and message delays are unpredictable. In this paper, we introduce asynchronous team automata (ATeams), which extend team automata with buffers to model asynchronous communication, in addition to conventional synchronous interaction. ATeams support individual interactions involving multiple senders and receivers, unlike well-known asynchronous models such as communicating finite-state machines and multi-party session types. We formalise the syntax and operational semantics of ATeams, study well-formedness and well-behavedness conditions, and present the prototypical A-Team tool that supports specification, animation and automated checks. This proposes ATeams as a unifying semantic foundation for modelling and analysis of heterogeneous synchronous–asynchronous multi-party interactions.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16557, pp. 27-49. Tokyo, Japan, 18–22 May 2026
DOI: 10.1007/978-3-032-26220-2_2
Project(s): Formal Methods in Software Engineering 2.0, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Basile Davide, Ter Beek Maurice H., Proença José
Team automata were introduced as a flexible extension of I/O automata to model collaborative behaviour in component-based and distributed systems. Their distinctive features include multi-party communication and a liberal synchronisation mechanism: components may jointly execute shared actions according to synchronisation policies that specify which subsets of components participate as senders or receivers. While this makes team automata well suited for modelling coordination, existing communication is synchronous and therefore insufficient for capturing certain behavioural aspects (e.g., due to message reordering) of modern networks and distributed systems, in which communication is typically asynchronous and message delays are unpredictable. In this paper, we introduce asynchronous team automata (ATeams), which extend team automata with buffers to model asynchronous communication, in addition to conventional synchronous interaction. ATeams support individual interactions involving multiple senders and receivers, unlike well-known asynchronous models such as communicating finite-state machines and multi-party session types. We formalise the syntax and operational semantics of ATeams, study well-formedness and well-behavedness conditions, and present the prototypical A-Team tool that supports specification, animation and automated checks. This proposes ATeams as a unifying semantic foundation for modelling and analysis of heterogeneous synchronous–asynchronous multi-party interactions.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16557, pp. 27-49. Tokyo, Japan, 18–22 May 2026
DOI: 10.1007/978-3-032-26220-2_2
Project(s): Formal Methods in Software Engineering 2.0, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
See at:
CNR IRIS | link.springer.com | CNR IRIS
2026
Journal article
Open Access
RebeCaos: a software artefact for Rebeca
Proença José, Ter Beek Maurice H.
We describe RebeCaos: a user-friendly web-based front-end tool for Rebeca, based on the Caos library for Scala. Rebeca is an actor-based language for modelling and analysing concurrent and distributed systems using reactive objects with no shared variables, asynchronous message passing with no blocking when sending and no explicit receiving, and unbounded message buffers for arriving messages. RebeCaos can simulate different operational semantics of (timed) Rebeca, thus facilitating the dissemination and awareness of Rebeca, providing insights into the differences among existing semantics for Rebeca, and supporting quick experimentation of new Rebeca variants (e.g., when the order of received messages is preserved or prioritised). RebeCaos also provides initial reachability analyses for Rebeca models (e.g., the possibility of reaching deadlocks or desirable states).Source: SCIENCE OF COMPUTER PROGRAMMING, vol. 254
DOI: 10.1016/j.scico.2026.103529
Metrics:
Proença José, Ter Beek Maurice H.
We describe RebeCaos: a user-friendly web-based front-end tool for Rebeca, based on the Caos library for Scala. Rebeca is an actor-based language for modelling and analysing concurrent and distributed systems using reactive objects with no shared variables, asynchronous message passing with no blocking when sending and no explicit receiving, and unbounded message buffers for arriving messages. RebeCaos can simulate different operational semantics of (timed) Rebeca, thus facilitating the dissemination and awareness of Rebeca, providing insights into the differences among existing semantics for Rebeca, and supporting quick experimentation of new Rebeca variants (e.g., when the order of received messages is preserved or prioritised). RebeCaos also provides initial reachability analyses for Rebeca models (e.g., the possibility of reaching deadlocks or desirable states).Source: SCIENCE OF COMPUTER PROGRAMMING, vol. 254
DOI: 10.1016/j.scico.2026.103529
Metrics:
See at:
CNR IRIS | www.sciencedirect.com | CNR IRIS
2025
Other
Open Access
Review on formal methods for software engineering: languages, methods, application domains
Ter Beek M. H.
Review on Formal Methods for Sotware Engineering: Languages, Methods, Application Domains by Markus Roggenbach, Antonio Cerone, Bernd-Holger Schlinglof, Gerardo Schneider, and Siraj Ahmed Shaikh Published by Springer, ISBN: 978-3-030-38799-0, 524 pages, 2022. https://doi.org/10.1007/978-3-030-38800-3Source: FORMAL ASPECTS OF COMPUTING, vol. 37 (issue 4), pp. 35:1-35:3
DOI: 10.1145/3746236
Metrics:
Ter Beek M. H.
Review on Formal Methods for Sotware Engineering: Languages, Methods, Application Domains by Markus Roggenbach, Antonio Cerone, Bernd-Holger Schlinglof, Gerardo Schneider, and Siraj Ahmed Shaikh Published by Springer, ISBN: 978-3-030-38799-0, 524 pages, 2022. https://doi.org/10.1007/978-3-030-38800-3Source: FORMAL ASPECTS OF COMPUTING, vol. 37 (issue 4), pp. 35:1-35:3
DOI: 10.1145/3746236
Metrics:
See at:
dl.acm.org | CNR IRIS | CNR IRIS | CNR IRIS
2025
Conference article
Open Access
Comparing the universal variability language with other textual variability modeling languages
Ter Beek M. H., Schmid K., Eichelberger H.
We compare the main features of the recently introduced Universal Variability Language (UVL) with other textual variability modeling languages from the software product line engineering domain. This comparison is structured according to the level of support that each language provides according to five dimensions: configurable elements, constraints, configuration, scalability, and formal semantics. This work extends our earlier work on comparing textual variability modeling languages that used a similar approach (Eichelberger and Schmid, 2015; ter Beek, Schmid, and Eichelberger, 2019).DOI: 10.1145/3748269.3749381
Project(s): Formal Methods in Software Engineering 2.0
Metrics:
Ter Beek M. H., Schmid K., Eichelberger H.
We compare the main features of the recently introduced Universal Variability Language (UVL) with other textual variability modeling languages from the software product line engineering domain. This comparison is structured according to the level of support that each language provides according to five dimensions: configurable elements, constraints, configuration, scalability, and formal semantics. This work extends our earlier work on comparing textual variability modeling languages that used a similar approach (Eichelberger and Schmid, 2015; ter Beek, Schmid, and Eichelberger, 2019).DOI: 10.1145/3748269.3749381
Project(s): Formal Methods in Software Engineering 2.0
Metrics:
See at:
dl.acm.org | CNR IRIS | CNR IRIS
2025
Book
Open Access
Preface to the proceedings of the 28th Brazilian symposium on formal methods: foundations and applications (SBMF 2025)
Ter Beek M. H., Teixeira L.
This book constitutes the refereed proceedings of the 28th Brazilian Symposium on Formal Methods: Foundations and Applications, SBMF 2025, held in Recife, Brazil, during December 3–5, 2025. The 12 full papers and 1 short paper included in this book were carefully reviewed and selected from 24 submissions. They were organized in topical sections as follows: Process Algebras and Time; Formal Verification; Testing; Availability and Contracts; Formal Methods and AI; and Teaching and Foundations.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16363, pp. i-xviii
DOI: 10.1007/978-3-032-12086-1
Metrics:
Ter Beek M. H., Teixeira L.
This book constitutes the refereed proceedings of the 28th Brazilian Symposium on Formal Methods: Foundations and Applications, SBMF 2025, held in Recife, Brazil, during December 3–5, 2025. The 12 full papers and 1 short paper included in this book were carefully reviewed and selected from 24 submissions. They were organized in topical sections as follows: Process Algebras and Time; Formal Verification; Testing; Availability and Contracts; Formal Methods and AI; and Teaching and Foundations.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16363, pp. i-xviii
DOI: 10.1007/978-3-032-12086-1
Metrics:
See at:
CNR IRIS | link.springer.com | CNR IRIS
2025
Journal article
Open Access
Model transformation and property preservation in rigorous software development: a systematic literature review
Jadoon G., Ter Beek M. H., Ferrari A.
Rigorous software development involves using highly structured methods and processes in software and system engineering to ensure that the developed products are correct, reliable, and robust. In this context, model-driven development (MDD) has emerged as a development paradigm that emphasizes designing software systems by means of graphical or textual models at different levels of abstraction, which capture different aspects or dimensions of the system-to-be. At the core of MDD is model transformation, which is the process of translating one model into another, according to specific rules. Property preservation in MDD refers to maintaining specific properties of the system model during transformations, including structural, behavioral, and domain-specific constraints. Over the past decades, research on model transformation and property preservation has seen several contributions. In this paper, we present a systematic literature review (SLR) to compile information on study demographics, model properties considered, techniques to ensure property preservation, and other aspects. In addition, through thematic analysis, we highlight significant challenges and benefits associated with model transformation and property preservation. We analyze 182 research studies published between 2000 and 2024. Most of the studies concern case studies (52) and rigorous analysis (47), while experimental studies using human subjects are limited (1). Formal logic is the most commonly used transformation language, used in 35 studies, while the Unified Modeling Language (UML) is also used for source (55) and target (21) modeling. A total of 93 of the studies performed system testing on models, while 44 of the studies used transformation rules to verify transformation properties. Among the verified model properties, 64 studies focused on consistency management, while 4 are related to model maintainability and reuse. We conclude from our SLR that property preservation could be improved by using model-specific verification methods and strategies based on the considered model artifacts. Our research also provides a relevant contribution by identifying the major challenges in MDD and proposing relevant solutions.Source: THE JOURNAL OF SYSTEMS AND SOFTWARE, vol. 230
DOI: 10.1016/j.jss.2025.112508
Metrics:
Jadoon G., Ter Beek M. H., Ferrari A.
Rigorous software development involves using highly structured methods and processes in software and system engineering to ensure that the developed products are correct, reliable, and robust. In this context, model-driven development (MDD) has emerged as a development paradigm that emphasizes designing software systems by means of graphical or textual models at different levels of abstraction, which capture different aspects or dimensions of the system-to-be. At the core of MDD is model transformation, which is the process of translating one model into another, according to specific rules. Property preservation in MDD refers to maintaining specific properties of the system model during transformations, including structural, behavioral, and domain-specific constraints. Over the past decades, research on model transformation and property preservation has seen several contributions. In this paper, we present a systematic literature review (SLR) to compile information on study demographics, model properties considered, techniques to ensure property preservation, and other aspects. In addition, through thematic analysis, we highlight significant challenges and benefits associated with model transformation and property preservation. We analyze 182 research studies published between 2000 and 2024. Most of the studies concern case studies (52) and rigorous analysis (47), while experimental studies using human subjects are limited (1). Formal logic is the most commonly used transformation language, used in 35 studies, while the Unified Modeling Language (UML) is also used for source (55) and target (21) modeling. A total of 93 of the studies performed system testing on models, while 44 of the studies used transformation rules to verify transformation properties. Among the verified model properties, 64 studies focused on consistency management, while 4 are related to model maintainability and reuse. We conclude from our SLR that property preservation could be improved by using model-specific verification methods and strategies based on the considered model artifacts. Our research also provides a relevant contribution by identifying the major challenges in MDD and proposing relevant solutions.Source: THE JOURNAL OF SYSTEMS AND SOFTWARE, vol. 230
DOI: 10.1016/j.jss.2025.112508
Metrics:
See at:
CNR IRIS | www.sciencedirect.com | CNR IRIS
2025
Other
Open Access
ISTI-day 2025 Proceedings
Del Corso G., Pedrotti A., Federico G., Gennaro C., Carrara F., Amato G., Di Benedetto M., Gabrielli E., Belli D., Matrullo Zoe, Miori V., Tolomei Gabriele, Waheed T., Marchetti E., Calabrò Antonello., Rossetti G., Stella Massimo, Cazabet Rémy, Abramski K., Cau E., Citraro S., Failla A., Mesina V., Morini V., Pansanella V., Colantonio S., Germanese D., Pascali M. A., Bianchi L., Messina N., Falchi F., Barsellotti L., Pacini G., Cassese M., Puccetti G., Esuli A., Volpi L., Moreo Alejandro, Sebastiani F., Sperduti G., Nguyen Dong, Broccia G., Ter Beek M. H., Ferrari A., Massink M., Belmonte Gina, Ciancia V., Papini O., Canapa G., Catricalà B., Manca M., Paternò F., Santoro C., Zedda E., Gallo S., Maenza S., Mattioli A., Simeoli L., Rucci D., Carlini E., Dazzi P., Kavalionak H., Mordacchini M., Rulli C., Muntean Cristina Ioana, Nardini F. M., Perego R., Rocchietti G., Lettich F., Renso C., Pugliese C., Casini G., Haldimann Jonas, Meyer Thomas, Assante M., Candela L., Dell'Amico A., Frosini L., Mangiacrapa F., Oliviero A., Pagano P., Panichi G., Peccerillo B., Procaccini M., Mannocci A., Manghi P., Lonetti F., Kang Dongjae, Di Giandomenico F., Jee Eunkyoung, Lazzini G., Conti F., Scopigno R., D'Acunto M., Moroni D., Cafiso M., Paradisi P., Callieri M., Pavoni G., Corsini M., De Falco A., Sala F., Saraceni Q., Gattiglia Gabriele
ISTI-Day is an annual information and networking event organized by the Institute of Information Science and Technologies "A. Faedo" (ISTI) of the Italian National Research Council (CNR). This event features an opening talk of the Director of the Dept. DIITET (Emilio F. Campana) as well as an overview of the Institute's activities presented by the ISTI Director (Roberto Scopigno). Those institutional segments are complemented by dedicated presentations and round tables featuring former staff members, as well as internal and external collaborators. To foster a network of knowledge and collaboration among newcomers, the 2025 ISTI Day edition also includes a large poster session that provides a comprehensive overview of current research activities. Each of the 13 laboratories contributes 1–3 posters, highlighting the most innovative work and offering early-career researchers a platform for discussion. Thus these proceedings include the posters selected for ISTI-Day 2025, reflecting the diverse and innovative nature of the Institute's research.
Del Corso G., Pedrotti A., Federico G., Gennaro C., Carrara F., Amato G., Di Benedetto M., Gabrielli E., Belli D., Matrullo Zoe, Miori V., Tolomei Gabriele, Waheed T., Marchetti E., Calabrò Antonello., Rossetti G., Stella Massimo, Cazabet Rémy, Abramski K., Cau E., Citraro S., Failla A., Mesina V., Morini V., Pansanella V., Colantonio S., Germanese D., Pascali M. A., Bianchi L., Messina N., Falchi F., Barsellotti L., Pacini G., Cassese M., Puccetti G., Esuli A., Volpi L., Moreo Alejandro, Sebastiani F., Sperduti G., Nguyen Dong, Broccia G., Ter Beek M. H., Ferrari A., Massink M., Belmonte Gina, Ciancia V., Papini O., Canapa G., Catricalà B., Manca M., Paternò F., Santoro C., Zedda E., Gallo S., Maenza S., Mattioli A., Simeoli L., Rucci D., Carlini E., Dazzi P., Kavalionak H., Mordacchini M., Rulli C., Muntean Cristina Ioana, Nardini F. M., Perego R., Rocchietti G., Lettich F., Renso C., Pugliese C., Casini G., Haldimann Jonas, Meyer Thomas, Assante M., Candela L., Dell'Amico A., Frosini L., Mangiacrapa F., Oliviero A., Pagano P., Panichi G., Peccerillo B., Procaccini M., Mannocci A., Manghi P., Lonetti F., Kang Dongjae, Di Giandomenico F., Jee Eunkyoung, Lazzini G., Conti F., Scopigno R., D'Acunto M., Moroni D., Cafiso M., Paradisi P., Callieri M., Pavoni G., Corsini M., De Falco A., Sala F., Saraceni Q., Gattiglia Gabriele
ISTI-Day is an annual information and networking event organized by the Institute of Information Science and Technologies "A. Faedo" (ISTI) of the Italian National Research Council (CNR). This event features an opening talk of the Director of the Dept. DIITET (Emilio F. Campana) as well as an overview of the Institute's activities presented by the ISTI Director (Roberto Scopigno). Those institutional segments are complemented by dedicated presentations and round tables featuring former staff members, as well as internal and external collaborators. To foster a network of knowledge and collaboration among newcomers, the 2025 ISTI Day edition also includes a large poster session that provides a comprehensive overview of current research activities. Each of the 13 laboratories contributes 1–3 posters, highlighting the most innovative work and offering early-career researchers a platform for discussion. Thus these proceedings include the posters selected for ISTI-Day 2025, reflecting the diverse and innovative nature of the Institute's research.
See at:
CNR IRIS | www.isti.cnr.it | CNR IRIS
2025
Book
Open Access
Preface to the proceedings of the 6th International conference on reliability, safety, and security of railway systems (RSSRail 2025)
Ter Beek M. H., Collart-Dutilleul S., Lecomte T.
This book constitutes the proceedings of the 6th International Conference, RSSRail 2025, in Pisa, Italy, during November 2025. The 12 full papers, 5 short papers, 3 short papers from invited speakers and 4 extended abstracts of journal-first papers presented here were carefully reviewed and selected from 35 submissions.They were focused on the following topical sections:Invited Presentations; AI & Planning; Surveys & Comparisons; Communication & Control; Industrial Experiences & Trams; Formal Modelling & Analysis.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16236, pp. i-xiii
DOI: 10.1007/978-3-032-10762-6
Project(s): Sustainable Mobility National Research Center
Metrics:
Ter Beek M. H., Collart-Dutilleul S., Lecomte T.
This book constitutes the proceedings of the 6th International Conference, RSSRail 2025, in Pisa, Italy, during November 2025. The 12 full papers, 5 short papers, 3 short papers from invited speakers and 4 extended abstracts of journal-first papers presented here were carefully reviewed and selected from 35 submissions.They were focused on the following topical sections:Invited Presentations; AI & Planning; Surveys & Comparisons; Communication & Control; Industrial Experiences & Trams; Formal Modelling & Analysis.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16236, pp. i-xiii
DOI: 10.1007/978-3-032-10762-6
Project(s): Sustainable Mobility National Research Center
Metrics:
See at:
CNR IRIS | link.springer.com | CNR IRIS
2025
Journal article
Open Access
Feature-oriented modelling and analysis of a self-adaptive robotic system
Päßler J., Ter Beek M. H., Damiani F., Dubslaff C., Johnsen E. B., Tapia Tarifa S. L.
Improved autonomy in robotic systems is needed for innovation in, e.g., the marine sector. Autonomous robots that are let loose in hazardous environments, such as underwater, need to handle uncertainties that stem from both their environment and internal state. While self-adaptation is crucial to cope with these uncertainties, bad decisions may cause the robot to get lost or even to cause severe environmental damage. Autonomous, self-adaptive robots that operate in uncontrolled environments full of uncertainties need to be reliable! Since these uncertainties are hard to replicate in test deployments, we need methods to formally analyse self-adaptive robots operating in uncontrolled environments. In this paper, we show how feature-oriented techniques can be used to formally model and analyse self-adaptive robotic systems in the presence of such uncertainties. Self-adaptive systems can be organised as two-layered systems with a managed subsystem handling the domain concerns and a managing subsystem implementing the adaptation logic. We consider a case study of an autonomous underwater vehicle (AUV) for pipeline inspection, in which the managed subsystem of the AUV is modelled as a family of systems, where each family member corresponds to a valid configuration of the AUV which can be seen as an operating mode of the AUV’s behaviour. The managing subsystem of the AUV is modelled as a control layer that is capable of dynamically switching between such valid configurations, depending on both environmental and internal uncertainties. These uncertainties are captured in a probabilistic and highly configurable model. Our modelling approach allows us to exploit powerful formal methods for feature-oriented systems, which we illustrate by analysing safety properties, energy consumption, and multi-objective properties, as well as performing parameter synthesis to analyse to what extent environmental conditions affect the AUV. The case study is realised in the probabilistic feature-oriented modelling language and verification tool ProFeat, and in particular exploits family-based probabilistic and parametric model checking.Source: FORMAL ASPECTS OF COMPUTING, vol. 37 (issue 4), pp. 32:1-32:39
DOI: 10.1145/3709159
Project(s): REMARO
, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Päßler J., Ter Beek M. H., Damiani F., Dubslaff C., Johnsen E. B., Tapia Tarifa S. L.
Improved autonomy in robotic systems is needed for innovation in, e.g., the marine sector. Autonomous robots that are let loose in hazardous environments, such as underwater, need to handle uncertainties that stem from both their environment and internal state. While self-adaptation is crucial to cope with these uncertainties, bad decisions may cause the robot to get lost or even to cause severe environmental damage. Autonomous, self-adaptive robots that operate in uncontrolled environments full of uncertainties need to be reliable! Since these uncertainties are hard to replicate in test deployments, we need methods to formally analyse self-adaptive robots operating in uncontrolled environments. In this paper, we show how feature-oriented techniques can be used to formally model and analyse self-adaptive robotic systems in the presence of such uncertainties. Self-adaptive systems can be organised as two-layered systems with a managed subsystem handling the domain concerns and a managing subsystem implementing the adaptation logic. We consider a case study of an autonomous underwater vehicle (AUV) for pipeline inspection, in which the managed subsystem of the AUV is modelled as a family of systems, where each family member corresponds to a valid configuration of the AUV which can be seen as an operating mode of the AUV’s behaviour. The managing subsystem of the AUV is modelled as a control layer that is capable of dynamically switching between such valid configurations, depending on both environmental and internal uncertainties. These uncertainties are captured in a probabilistic and highly configurable model. Our modelling approach allows us to exploit powerful formal methods for feature-oriented systems, which we illustrate by analysing safety properties, energy consumption, and multi-objective properties, as well as performing parameter synthesis to analyse to what extent environmental conditions affect the AUV. The case study is realised in the probabilistic feature-oriented modelling language and verification tool ProFeat, and in particular exploits family-based probabilistic and parametric model checking.Source: FORMAL ASPECTS OF COMPUTING, vol. 37 (issue 4), pp. 32:1-32:39
DOI: 10.1145/3709159
Project(s): REMARO
, Typeful Language Adaptation for Dynamic, Interacting and Evolving SystemsMetrics:
See at:
dl.acm.org | CNR IRIS | CNR IRIS | CNR IRIS
2025
Conference article
Open Access
Integrating testing with runtime verification for mission-critical distributed control systems
Ancona D., Avola S., Ferrando A., Baglietto P., Ter Beek M. H., Parodi A., Camera G., Pinasco M.
The verification of safety properties of mission-critical Distributed Control Systems (DCS) is challenging, especially when they depend on a dynamically varying number of distributed components interacting through the system's Integration Layer (IL). In such cases, complementing testing with Runtime Verification (RV) can be beneficial to detect non-systematic errors at earlier stages and reduce the time-to-production. We adopt RV to test the IL of a real-world mission-critical railway control system, based on a Message-oriented Middleware (MoM) implementing a publish-subscribe communication protocol, with critical requirements on the uniqueness and order of the exchanged messages. These requirements are formalized in RML (Runtime Monitoring Language) and compiled into a monitor which verifies them dynamically. Performance measurements on real-world scenario parameters show that our approach can complement testing in the Continuous Integration (CI) cycle.DOI: 10.1109/dsn-s65789.2025.00056
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Ancona D., Avola S., Ferrando A., Baglietto P., Ter Beek M. H., Parodi A., Camera G., Pinasco M.
The verification of safety properties of mission-critical Distributed Control Systems (DCS) is challenging, especially when they depend on a dynamically varying number of distributed components interacting through the system's Integration Layer (IL). In such cases, complementing testing with Runtime Verification (RV) can be beneficial to detect non-systematic errors at earlier stages and reduce the time-to-production. We adopt RV to test the IL of a real-world mission-critical railway control system, based on a Message-oriented Middleware (MoM) implementing a publish-subscribe communication protocol, with critical requirements on the uniqueness and order of the exchanged messages. These requirements are formalized in RML (Runtime Monitoring Language) and compiled into a monitor which verifies them dynamically. Performance measurements on real-world scenario parameters show that our approach can complement testing in the Continuous Integration (CI) cycle.DOI: 10.1109/dsn-s65789.2025.00056
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
See at:
CNR IRIS | ieeexplore.ieee.org | CNR IRIS | CNR IRIS
2025
Journal article
Open Access
Models for formal methods and tools: the case of railway systems
Ter Beek M. H.
Formal methods and tools are successfully applied to the development of safety-critical systems for decades now, in particular in the transport domain, without a single technique or tool emerging as the dominant solution for system design. Formal methods are highly recommended by the existing safety standards in the railway industry, but railway engineers typically lack the knowledge to transform their semi-formal models into a formal model, with a precise semantics, that can serve as input to formal methods tools. We share the results of performing empirical studies in the field, including usability analyses of formal methods tools involving railway practitioners. We discuss, in particular with respect to railway systems and their modelling, our experiences in applying formal methods and tools to a variety of case studies, for which we interacted with a number of companies from the railway domain. We report on lessons learned from these experiences and provide pointers to steer future research towards facilitating further synergies between researchers and developers of formal methods and tools on the one hand and practitioners from the railway industry on the other.Source: SOFTWARE AND SYSTEMS MODELING, vol. 24 (issue 6), pp. 1935-1954
DOI: 10.1007/s10270-025-01276-3
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
Ter Beek M. H.
Formal methods and tools are successfully applied to the development of safety-critical systems for decades now, in particular in the transport domain, without a single technique or tool emerging as the dominant solution for system design. Formal methods are highly recommended by the existing safety standards in the railway industry, but railway engineers typically lack the knowledge to transform their semi-formal models into a formal model, with a precise semantics, that can serve as input to formal methods tools. We share the results of performing empirical studies in the field, including usability analyses of formal methods tools involving railway practitioners. We discuss, in particular with respect to railway systems and their modelling, our experiences in applying formal methods and tools to a variety of case studies, for which we interacted with a number of companies from the railway domain. We report on lessons learned from these experiences and provide pointers to steer future research towards facilitating further synergies between researchers and developers of formal methods and tools on the one hand and practitioners from the railway industry on the other.Source: SOFTWARE AND SYSTEMS MODELING, vol. 24 (issue 6), pp. 1935-1954
DOI: 10.1007/s10270-025-01276-3
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
See at:
CNR IRIS | link.springer.com | CNR IRIS