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
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
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 Z., Miori V., Tolomei G., Waheed T., Marchetti E., Calabrò A., Rossetti G., Stella M., Cazabet R., 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 A., Sebastiani F., Sperduti G., Nguyen D., Broccia G., Ter Beek M. H., Ferrari A., Massink M., Belmonte G., 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 J., Meyer T., 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 D., Di Giandomenico F., Jee E., 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 G.
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 Z., Miori V., Tolomei G., Waheed T., Marchetti E., Calabrò A., Rossetti G., Stella M., Cazabet R., 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 A., Sebastiani F., Sperduti G., Nguyen D., Broccia G., Ter Beek M. H., Ferrari A., Massink M., Belmonte G., 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 J., Meyer T., 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 D., Di Giandomenico F., Jee E., 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 G.
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
2025
Conference article
Open Access
RebeCaos
Proença J., Ter Beek M. H.
We describe RebeCaos, a user-friendly web-based front-end tool for the Rebeca language, based on the Caos library for Scala. 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). The tool also comes with initial reachability analyses for Rebeca models (e.g., the possibility of reaching deadlocks or desirable states). We illustrate the RebeCaos tool by means of a ticket service use case from the timed Rebeca literature.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15731, pp. 219-229. Lille, France, 17-19 giugno 2025
DOI: 10.1007/978-3-031-95589-1_11
Project(s): Formal Methods in Software Engineering 2.0, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Proença J., Ter Beek M. H.
We describe RebeCaos, a user-friendly web-based front-end tool for the Rebeca language, based on the Caos library for Scala. 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). The tool also comes with initial reachability analyses for Rebeca models (e.g., the possibility of reaching deadlocks or desirable states). We illustrate the RebeCaos tool by means of a ticket service use case from the timed Rebeca literature.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15731, pp. 219-229. Lille, France, 17-19 giugno 2025
DOI: 10.1007/978-3-031-95589-1_11
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 | CNR IRIS
2025
Other
Restricted
CN MOST SP4 D1.3.5: Report on assessed methods and models for resilient and sustainable railway infrastructures
D’acierno L., De Matteis L., Basile D., Ter Beek M., Chiaradonna S., Di Giandomenico F., Gregori M., Furini F, D’alfonso T, Matteucci G., Barbaro M., Collina A., Team Of Ferrovie Nord, Team Of Almaviva
This deliverable contains a description of the technical work carried out in Task 1.3 (Resilient and sustainable railway infrastructure) of WP1 (Increase in capacity of railway transport) within Spoke 4 (Rail Transport) of the Italian National Centre for Sustainable Mobility (CN-MOST). In particular, the document presents the work carried out by UNINA, CNR, UNIROMA1, POLIMI, FN and ALMAVIVA concerning the assessed methods and models for resilient and sustainable railway infrastructures.Project(s): CN MOST (National Sustainable Mobility Centre) Spoke 4: Rail Transportation
D’acierno L., De Matteis L., Basile D., Ter Beek M., Chiaradonna S., Di Giandomenico F., Gregori M., Furini F, D’alfonso T, Matteucci G., Barbaro M., Collina A., Team Of Ferrovie Nord, Team Of Almaviva
This deliverable contains a description of the technical work carried out in Task 1.3 (Resilient and sustainable railway infrastructure) of WP1 (Increase in capacity of railway transport) within Spoke 4 (Rail Transport) of the Italian National Centre for Sustainable Mobility (CN-MOST). In particular, the document presents the work carried out by UNINA, CNR, UNIROMA1, POLIMI, FN and ALMAVIVA concerning the assessed methods and models for resilient and sustainable railway infrastructures.Project(s): CN MOST (National Sustainable Mobility Centre) Spoke 4: Rail Transportation
2025
Conference article
Open Access
Analysing self-adaptive systems as software product lines
Päßler J., Ter Beek M. H., Damiani F., Johnsen E. B., Tapia Tarifa S. L.
This one-page document summarises a paper published in JSS (Päßler et al., 2025).DOI: 10.1145/3744915.3748483
Metrics:
Päßler J., Ter Beek M. H., Damiani F., Johnsen E. B., Tapia Tarifa S. L.
This one-page document summarises a paper published in JSS (Päßler et al., 2025).DOI: 10.1145/3744915.3748483
Metrics:
See at:
dl.acm.org | CNR IRIS | CNR IRIS
2025
Contribution to book
Open Access
Controlled hybrid CD grammar systems
Ter Beek M. H.
We study the generative power of hybrid CD grammar systems whose derivations are controlled by a graph, a hypothesis language or a generalized sequential machine. We relate them to the families of languages generated by matrix grammars with appearance checking. We thus characterise language families that lie in between that of the families of context-free and context-sensitive languages, which are of particular interest to linguists. In particular, we show that controlled hybrid CD grammar systems can generate the non-context-free features multiple agreements, crossed agreements and (re)duplication that occur in many natural languages.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15840, pp. 3-25
DOI: 10.1007/978-3-031-97274-4_1
Metrics:
Ter Beek M. H.
We study the generative power of hybrid CD grammar systems whose derivations are controlled by a graph, a hypothesis language or a generalized sequential machine. We relate them to the families of languages generated by matrix grammars with appearance checking. We thus characterise language families that lie in between that of the families of context-free and context-sensitive languages, which are of particular interest to linguists. In particular, we show that controlled hybrid CD grammar systems can generate the non-context-free features multiple agreements, crossed agreements and (re)duplication that occur in many natural languages.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15840, pp. 3-25
DOI: 10.1007/978-3-031-97274-4_1
Metrics:
See at:
CNR IRIS | link.springer.com | CNR IRIS | CNR IRIS
2025
Conference 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.
This one-page document summarises a paper published in FAC (Päßler et al., 2025).DOI: 10.1145/3744915.3748484
Metrics:
Päßler J., Ter Beek M. H., Damiani F., Dubslaff C., Johnsen E. B., Tapia Tarifa S. L.
This one-page document summarises a paper published in FAC (Päßler et al., 2025).DOI: 10.1145/3744915.3748484
Metrics:
See at:
dl.acm.org | CNR IRIS | CNR IRIS
2025
Contribution to book
Open Access
Animating Rebeca
Ter Beek M., Proença J.
Rebeca is 20+ years old. Introduced by Marjan Sirjani and colleagues for modelling and analysing actor-based systems, it comes with a variety of tool support, including dedicated model checkers, simulators, and code generators. When encountering Rebeca for the first time, either as a student, as a researcher, or as a practitioner from industry, one needs to grasp the subtleties of Rebeca's semantics, which includes variants with probabilities and time. This paper presents a user-friendly web-based front-end, based on the Caos library for Scala, to animate different operational semantics of (timed) Rebeca. This can facilitate the dissemination and awareness of Rebeca, provide insights into the differences among existing semantics, and support quick experimentation of new variants (e.g., when the order of received messages is preserved). The tool is illustrated by means of a ticket service use case from the literature.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15560, pp. 182-194
DOI: 10.1007/978-3-031-85134-6_8
Project(s): Formal Methods in Software Engineering 2.0, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Ter Beek M., Proença J.
Rebeca is 20+ years old. Introduced by Marjan Sirjani and colleagues for modelling and analysing actor-based systems, it comes with a variety of tool support, including dedicated model checkers, simulators, and code generators. When encountering Rebeca for the first time, either as a student, as a researcher, or as a practitioner from industry, one needs to grasp the subtleties of Rebeca's semantics, which includes variants with probabilities and time. This paper presents a user-friendly web-based front-end, based on the Caos library for Scala, to animate different operational semantics of (timed) Rebeca. This can facilitate the dissemination and awareness of Rebeca, provide insights into the differences among existing semantics, and support quick experimentation of new variants (e.g., when the order of received messages is preserved). The tool is illustrated by means of a ticket service use case from the literature.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15560, pp. 182-194
DOI: 10.1007/978-3-031-85134-6_8
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 | CNR IRIS
2025
Contribution to book
Open Access
Formal methods for intersymbolic AI
Ter Beek M. H., Dubslaff C., Schaefer I.
A key benefit of symbolic (rule-based) artificial intelligence (AI) is its formal rigor, which comes at the cost of formal modeling effort and computational expensive reasoning. Differently, subsymbolic (datadriven) AI approaches usually outperform rigorous ones in performance but might lead to unsound results. Intersymbolic AI is an emerging field in AI that aims to combine symbolic and subsymbolic AI approaches, exploiting the benefits from both worlds. The scope of the ISoLA 2025 track on "Formal Methods for Intersymbolic AI" is to gather researchers and practitioners from formal methods and (sub)symbolic AI to establish the boundaries of intersymbolic AI and to investigate and clarify the role of formal methods therein.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16220, pp. xvii-xx
Ter Beek M. H., Dubslaff C., Schaefer I.
A key benefit of symbolic (rule-based) artificial intelligence (AI) is its formal rigor, which comes at the cost of formal modeling effort and computational expensive reasoning. Differently, subsymbolic (datadriven) AI approaches usually outperform rigorous ones in performance but might lead to unsound results. Intersymbolic AI is an emerging field in AI that aims to combine symbolic and subsymbolic AI approaches, exploiting the benefits from both worlds. The scope of the ISoLA 2025 track on "Formal Methods for Intersymbolic AI" is to gather researchers and practitioners from formal methods and (sub)symbolic AI to establish the boundaries of intersymbolic AI and to investigate and clarify the role of formal methods therein.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16220, pp. xvii-xx
See at:
CNR IRIS | link.springer.com | CNR IRIS
2025
Other
Restricted
PRIN PNRR Adventure D2: Report on the definition of methods for qualitative and quantitative evaluation of KPIs of railway systems
Basile D., Ter Beek M., Carnevali L., Chiaradonna S., Di Giandomenico F., Fantechi A., Gori G.
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 of energy saving and taking into account failures, criticalities, and priorities of the system under analysis. The developed solutions are going to be 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 details the techniques that have been considered and the advancements.Project(s): ADVancEd iNtegraTed evalUation of Railway systEms
Basile D., Ter Beek M., Carnevali L., Chiaradonna S., Di Giandomenico F., Fantechi A., Gori G.
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 of energy saving and taking into account failures, criticalities, and priorities of the system under analysis. The developed solutions are going to be 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 details the techniques that have been considered and the advancements.Project(s): ADVancEd iNtegraTed evalUation of Railway systEms