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
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
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 
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
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
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
Contribution to book
Restricted
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 | CNR IRIS | CNR IRIS | link.springer.com
2024
Journal article
Open Access
Product lines of dataflows
Lienhardt M, Ter Beek Mh, Damiani F
Data-centric parallel programming models such as dataflows are well established to implement complex concurrent software. However, in a context of a configurable software, the dataflow used in its computation might vary with respect to the selected options: this happens in particular in fields such as Computational Fluid Dynamics (CFD), where the shape of the domain in which the fluid flows and the equations used to simulate the flow are all options configuring the dataflow to execute.In this paper, we present an approach to implement product lines of dataflows, based on Delta-Oriented Programming (DOP) and term rewriting. This approach includes several analyses to check that all dataflows of a product line can be generated. Moreover, we discuss a prototype implementation of the approach and demonstrate its feasibility in practice.Source: THE JOURNAL OF SYSTEMS AND SOFTWARE, vol. 210
DOI: 10.1016/j.jss.2023.111928
Metrics:
Lienhardt M, Ter Beek Mh, Damiani F
Data-centric parallel programming models such as dataflows are well established to implement complex concurrent software. However, in a context of a configurable software, the dataflow used in its computation might vary with respect to the selected options: this happens in particular in fields such as Computational Fluid Dynamics (CFD), where the shape of the domain in which the fluid flows and the equations used to simulate the flow are all options configuring the dataflow to execute.In this paper, we present an approach to implement product lines of dataflows, based on Delta-Oriented Programming (DOP) and term rewriting. This approach includes several analyses to check that all dataflows of a product line can be generated. Moreover, we discuss a prototype implementation of the approach and demonstrate its feasibility in practice.Source: THE JOURNAL OF SYSTEMS AND SOFTWARE, vol. 210
DOI: 10.1016/j.jss.2023.111928
Metrics:
See at:
CNR IRIS | ISTI Repository | ISTI Repository | www.sciencedirect.com | CNR IRIS | CNR IRIS
2024
Conference article
Open Access
X-by-Construction meets AI
Ter Beek M. H., Cleophas L., Dubslaff C., Schaefer I.
During the past decade, researchers have investigated X-by-Construction (XbC), encompassing extensions beyond correctness concerns as in the more traditional Correctness-by-Construction (CbC) paradigm. Like CbC, XbC is a refinement approach to engineer systems that by-construction satisfy certain properties (e.g., non-functional ones in the case of XbC)—also, and in particular, in the setting of probabilistic systems and properties, and both at design time and at runtime. In line with the need to integrate concepts from artificial intelligence (AI), this track brings together researchers and practitioners to share their views on the many possible synergies between CbC/XbC and AI.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15222, pp. 155-161. Crete, Greece, 27-31/10/2024
DOI: 10.1007/978-3-031-75387-9_10
Metrics:
Ter Beek M. H., Cleophas L., Dubslaff C., Schaefer I.
During the past decade, researchers have investigated X-by-Construction (XbC), encompassing extensions beyond correctness concerns as in the more traditional Correctness-by-Construction (CbC) paradigm. Like CbC, XbC is a refinement approach to engineer systems that by-construction satisfy certain properties (e.g., non-functional ones in the case of XbC)—also, and in particular, in the setting of probabilistic systems and properties, and both at design time and at runtime. In line with the need to integrate concepts from artificial intelligence (AI), this track brings together researchers and practitioners to share their views on the many possible synergies between CbC/XbC and AI.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15222, pp. 155-161. Crete, Greece, 27-31/10/2024
DOI: 10.1007/978-3-031-75387-9_10
Metrics:
See at:
IRIS Cnr | IRIS Cnr | IRIS Cnr | doi.org | CNR IRIS | CNR IRIS | Eindhoven University of Technology Research Portal
2024
Book
Open Access
SPLC '24: Proceedings of the 28th ACM International Systems and Software Product Line Conference
Cordy M., Strüber D., Pinto M., Groher I., Dhungana D., Krüger J., Alves Pereira J., Acher M., Thüm T., Ter Beek M., Galasso-Carbonnel J., Arcaini P., Mousavi M. R., Tërnava X., Galindo J., Yue T., Fuentes L., Horcas F. M.
Welcome to the 28th ACM International Systems and Software Product Line Conference (SPLC 2024). SPLC is a thriving ground for practitioners, researchers, and educators working in areas related to systems and software product lines. With the increasing size and complexity of software, efficiently supporting software processes becomes an extremely important task. SPLC 2024 acted as a venue fostering knowledge exchange and learning about the state of the art in software product lines as well as new practices, trends, innovations, insights from industrial applications, and new challenges.DOI: 10.1145/3646548
Metrics:
Cordy M., Strüber D., Pinto M., Groher I., Dhungana D., Krüger J., Alves Pereira J., Acher M., Thüm T., Ter Beek M., Galasso-Carbonnel J., Arcaini P., Mousavi M. R., Tërnava X., Galindo J., Yue T., Fuentes L., Horcas F. M.
Welcome to the 28th ACM International Systems and Software Product Line Conference (SPLC 2024). SPLC is a thriving ground for practitioners, researchers, and educators working in areas related to systems and software product lines. With the increasing size and complexity of software, efficiently supporting software processes becomes an extremely important task. SPLC 2024 acted as a venue fostering knowledge exchange and learning about the state of the art in software product lines as well as new practices, trends, innovations, insights from industrial applications, and new challenges.DOI: 10.1145/3646548
Metrics:
See at:
dl.acm.org | CNR IRIS | doi.org | CNR IRIS
2024
Conference article
Open Access
Assessing the understandability and acceptance of attack-defense trees for modelling security requirements
Broccia G., Ter Beek M. H., Lluch Lafuente A., Spoletini P., Ferrari A.
Context and Motivation Attack-Defense Trees (ADTs) are a graphical notation used to model and assess security requirements. ADTs are widely popular, as they can facilitate communication between differ-ent stakeholders involved in system security evaluation, and they are for-mal enough to be verified, e.g., with model checkers. Question/Problem While the quality of this notation has been primarily assessed quanti-tatively, its understandability has never been evaluated despite being mentioned as a key factor for its success. Principal idea/Results In this paper, we conduct an experiment with 25 human subjects to assess the understandability and user acceptance of the ADT notation. The study focuses on performance-based variables and perception-based variables, with the aim of evaluating the relationship between these measures and how they might impact the practical use of the notation. The results confirm a good level of understandability of ADTs. Participants consider them useful, and they show intention to use them. Contribution This is the first study empirically supporting the understandability of ADTs, thereby contributing to the theory of security requirements engineering.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14588, pp. 39-56. Winterthur, Switzerland, April 8–11, 2024
DOI: 10.1007/978-3-031-57327-9_3
DOI: 10.48550/arxiv.2404.06386
Project(s): CODECS, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Broccia G., Ter Beek M. H., Lluch Lafuente A., Spoletini P., Ferrari A.
Context and Motivation Attack-Defense Trees (ADTs) are a graphical notation used to model and assess security requirements. ADTs are widely popular, as they can facilitate communication between differ-ent stakeholders involved in system security evaluation, and they are for-mal enough to be verified, e.g., with model checkers. Question/Problem While the quality of this notation has been primarily assessed quanti-tatively, its understandability has never been evaluated despite being mentioned as a key factor for its success. Principal idea/Results In this paper, we conduct an experiment with 25 human subjects to assess the understandability and user acceptance of the ADT notation. The study focuses on performance-based variables and perception-based variables, with the aim of evaluating the relationship between these measures and how they might impact the practical use of the notation. The results confirm a good level of understandability of ADTs. Participants consider them useful, and they show intention to use them. Contribution This is the first study empirically supporting the understandability of ADTs, thereby contributing to the theory of security requirements engineering.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14588, pp. 39-56. Winterthur, Switzerland, April 8–11, 2024
DOI: 10.1007/978-3-031-57327-9_3
DOI: 10.48550/arxiv.2404.06386
Project(s): CODECS
, Typeful Language Adaptation for Dynamic, Interacting and Evolving SystemsMetrics:
See at:
arXiv.org e-Print Archive | doi.org | doi.org | IRIS Cnr | CNR IRIS | CNR IRIS | IRIS Cnr
2024
Journal article
Open Access
Formal methods in industry
Ter Beek M. H., Chapman R., Cleaveland R., Garavel H., Gu R., Ter Horst I., Keiren J. J. A., Lecomte T., Leuschel M., Rozier K. Y., Sampaio A., Seceleanu C., Thomas M., Willemse T. A. C., Zhang L.
Formal methods encompass a wide choice of techniques and tools for the specification, development, analysis, and verification of software and hardware systems. Formal methods are widely applied in industry, in activities ranging from the elicitation of requirements and the early design phases all the way to the deployment, configuration, and runtime monitoring of actual systems. Formal methods allow one to precisely specify the environment in which a system operates, the requirements and properties that the system should satisfy, the models of the system used during the various design steps, and the code embedded in the final implementation, as well as to express conformance relations between these specifications. We present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain, like railways and other transportation systems, but also covering other areas such as lithography manufacturing and cloud security in e-commerce, to name but a few. We also report testimonies from a number of representatives from industry who, either directly or indirectly, use or have used formal methods in their industrial project endeavours. These persons are spread geographically, including Europe, Asia, North and South America, and the involved projects witness the large coverage of applications of formal methods, not limited to the safety-critical domain. We thus make a case for the importance of formal methods, and in particular of the capacity to abstract and mathematical reasoning that are taught as part of any formal methods course. These are fundamental Computer Science skills that graduates should profit from when working as computer scientists in industry, as confirmed by industry representatives.Source: FORMAL ASPECTS OF COMPUTING, vol. 37 (issue 1), pp. 1-38
DOI: 10.1145/3689374
Metrics:
Ter Beek M. H., Chapman R., Cleaveland R., Garavel H., Gu R., Ter Horst I., Keiren J. J. A., Lecomte T., Leuschel M., Rozier K. Y., Sampaio A., Seceleanu C., Thomas M., Willemse T. A. C., Zhang L.
Formal methods encompass a wide choice of techniques and tools for the specification, development, analysis, and verification of software and hardware systems. Formal methods are widely applied in industry, in activities ranging from the elicitation of requirements and the early design phases all the way to the deployment, configuration, and runtime monitoring of actual systems. Formal methods allow one to precisely specify the environment in which a system operates, the requirements and properties that the system should satisfy, the models of the system used during the various design steps, and the code embedded in the final implementation, as well as to express conformance relations between these specifications. We present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain, like railways and other transportation systems, but also covering other areas such as lithography manufacturing and cloud security in e-commerce, to name but a few. We also report testimonies from a number of representatives from industry who, either directly or indirectly, use or have used formal methods in their industrial project endeavours. These persons are spread geographically, including Europe, Asia, North and South America, and the involved projects witness the large coverage of applications of formal methods, not limited to the safety-critical domain. We thus make a case for the importance of formal methods, and in particular of the capacity to abstract and mathematical reasoning that are taught as part of any formal methods course. These are fundamental Computer Science skills that graduates should profit from when working as computer scientists in industry, as confirmed by industry representatives.Source: FORMAL ASPECTS OF COMPUTING, vol. 37 (issue 1), pp. 1-38
DOI: 10.1145/3689374
Metrics:
See at:
IRIS Cnr | Formal Aspects of Computing | IRIS Cnr | INRIA2 | Hal | INRIA2 | CNR IRIS | CNR IRIS
2024
Journal article
Embargo
Advancing orchestration synthesis for contract automata
Basile D., Ter Beek M.
Contract automata allow to formally define the behaviour of service contracts in terms of service offers and requests, some of which are moreover optional and some of which are necessary. A composition of contracts is said to be in agreement if all service requests are matched by corresponding offers. Whenever a composition of contracts is not in agreement, it can be refined to reach an agreement using the orchestration synthesis algorithm. This algorithm is a variant of the synthesis algorithm used in supervisory control theory and it is based on the fact that optional transitions are controllable, whereas necessary transitions are at most semi-controllable and cannot always be controlled. In this paper, we present advancements of the orchestration synthesis for contract automata. Notably, we identify the existing limits of the orchestration synthesis and propose a novel orchestration synthesis along with additional constructs to enhance the expressiveness and scalability of contract automata. The proposed advancements have been implemented and experimented on two case studies, one of which originates from the railway domain and the other is a card game.Source: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, vol. 141
DOI: 10.1016/j.jlamp.2024.100998
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
Basile D., Ter Beek M.
Contract automata allow to formally define the behaviour of service contracts in terms of service offers and requests, some of which are moreover optional and some of which are necessary. A composition of contracts is said to be in agreement if all service requests are matched by corresponding offers. Whenever a composition of contracts is not in agreement, it can be refined to reach an agreement using the orchestration synthesis algorithm. This algorithm is a variant of the synthesis algorithm used in supervisory control theory and it is based on the fact that optional transitions are controllable, whereas necessary transitions are at most semi-controllable and cannot always be controlled. In this paper, we present advancements of the orchestration synthesis for contract automata. Notably, we identify the existing limits of the orchestration synthesis and propose a novel orchestration synthesis along with additional constructs to enhance the expressiveness and scalability of contract automata. The proposed advancements have been implemented and experimented on two case studies, one of which originates from the railway domain and the other is a card game.Source: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, vol. 141
DOI: 10.1016/j.jlamp.2024.100998
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
See at:
Journal of Logical and Algebraic Methods in Programming | IRIS Cnr | CNR IRIS | IRIS Cnr
2024
Conference article
Open Access
An integrated perspective on the evaluation of complex railway systems
Basile D., Ter Beek M. H., Carnevali L., Chiaradonna S., Di Giandomenico F., Fantechi A., Gori G.
The project ADVENTURE (ADVancEd iNtegraTed evalUation of Railway systEms) aims to provide novel solutions for the evaluation of RAMS requirements as well as to present trade-offs between dependability attributes and energy consumption in complex railway systems, leveraging both qualitative and quantitative evaluation methods. To this end, case studies concerning distributed interlocking systems, standard interfaces, and railroad switch heaters are considered, comprising different challenging scenarios, notably representative of the complexity of railway systems. In this paper, we illustrate the objectives of the project and the activities planned to address them, devising future steps to integrate the envisaged contributions within a unified framework.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15223, pp. 190-207. Crete, Greece, 27-31/10/2024
DOI: 10.1007/978-3-031-75390-9_13
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
Basile D., Ter Beek M. H., Carnevali L., Chiaradonna S., Di Giandomenico F., Fantechi A., Gori G.
The project ADVENTURE (ADVancEd iNtegraTed evalUation of Railway systEms) aims to provide novel solutions for the evaluation of RAMS requirements as well as to present trade-offs between dependability attributes and energy consumption in complex railway systems, leveraging both qualitative and quantitative evaluation methods. To this end, case studies concerning distributed interlocking systems, standard interfaces, and railroad switch heaters are considered, comprising different challenging scenarios, notably representative of the complexity of railway systems. In this paper, we illustrate the objectives of the project and the activities planned to address them, devising future steps to integrate the envisaged contributions within a unified framework.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15223, pp. 190-207. Crete, Greece, 27-31/10/2024
DOI: 10.1007/978-3-031-75390-9_13
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
See at:
IRIS Cnr | IRIS Cnr | IRIS Cnr | Flore (Florence Research Repository) | Flore (Florence Research Repository) | CNR IRIS | CNR IRIS
2024
Journal article
Open Access
Sustainable mobility: increase of capacity and digitisation of railway transport
Davide Basile, Maurice Ter Beek, Alessio Ferrari
Researchers from the Formal Methods and Tools (FMT) lab of CNR–ISTI work on the increase of capacity and digitisation of railway transport. The research is conducted in the context of the NextGenerationEU-funded project on “Railway Transportation” (Spoke 4), which is part of the National Centre for Sustainable Mobility (MOST).Source: ERCIM NEWS, vol. 138, pp. 8-9
Project(s): CN MOST (National Sustainable Mobility Centre) Spoke 4: Rail Transportation
Davide Basile, Maurice Ter Beek, Alessio Ferrari
Researchers from the Formal Methods and Tools (FMT) lab of CNR–ISTI work on the increase of capacity and digitisation of railway transport. The research is conducted in the context of the NextGenerationEU-funded project on “Railway Transportation” (Spoke 4), which is part of the National Centre for Sustainable Mobility (MOST).Source: ERCIM NEWS, vol. 138, pp. 8-9
Project(s): CN MOST (National Sustainable Mobility Centre) Spoke 4: Rail Transportation
See at:
ercim-news.ercim.eu | CNR IRIS | CNR IRIS
2024
Conference article
Open Access
Formal methods and tools applied in the railway domain
Ter Beek M. H.
ABZ and other state-based 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 language or tool emerging as the dominant solution for system design. Formal methods are highly recommended by the current safety standards in the railway industry, but railway engineers often lack the knowledge to transform their semi-formal models into formal models, with a precise semantics, to serve as input to formal methods tools. We share the results of performing empirical studies in the railway domain, 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 rigorous state-based 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 drive future research towards facilitating further synergies between—on the one hand—researchers and developers of ABZ and other state-based formal methods and tools, and—on the other hand—practitioners from the railway industry.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14759, pp. 3-21. Bergamo, Italy, 25-28/06/2024
DOI: 10.1007/978-3-031-63790-2_1
Metrics:
Ter Beek M. H.
ABZ and other state-based 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 language or tool emerging as the dominant solution for system design. Formal methods are highly recommended by the current safety standards in the railway industry, but railway engineers often lack the knowledge to transform their semi-formal models into formal models, with a precise semantics, to serve as input to formal methods tools. We share the results of performing empirical studies in the railway domain, 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 rigorous state-based 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 drive future research towards facilitating further synergies between—on the one hand—researchers and developers of ABZ and other state-based formal methods and tools, and—on the other hand—practitioners from the railway industry.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14759, pp. 3-21. Bergamo, Italy, 25-28/06/2024
DOI: 10.1007/978-3-031-63790-2_1
Metrics:
See at:
CNR IRIS | link.springer.com | doi.org | CNR IRIS | CNR IRIS
2024
Journal article
Open Access
The role of Formal Methods in Computer Science education
Ter Beek M., Broy M., Dongol B.
This piece points out the key position of formal methods in Computer Science (CS) education, which must thus be reflected in any CS curriculum as a knowledge area rather than as elective topics in distinct knowledge areas. This is confirmed by the increasing use of formal methods in industry (ter Beek et al., 2024) - not limited to safety-critical domains. First, we indicate the importance of formal methods thinking in CS education (Dongol et al., 2024), since this provides the necessary rigor in reasoning about software, its specification, its verification, and its correctness - all fundamental skills for future software developers. Then, we argue that every computer scientist needs to know formal methods (Broy et al., 2024), since the skills and knowledge acquired in this way provide the indispensable solid foundation that forms the backbone of CS practice. Finally, we underline that teaching formal methods need not come at the cost of displacing other engineering aspects of CS that are already widely accepted as essential. On the contrary, formal methods have the potential to support and strengthen the presentation and knowledge in all these subdisciplines. We provide suggestions for educators on how to incorporate formal methods into CS education.Source: ACM INROADS, vol. 15 (issue 4), pp. 58-66
DOI: 10.1145/3702231
Metrics:
Ter Beek M., Broy M., Dongol B.
This piece points out the key position of formal methods in Computer Science (CS) education, which must thus be reflected in any CS curriculum as a knowledge area rather than as elective topics in distinct knowledge areas. This is confirmed by the increasing use of formal methods in industry (ter Beek et al., 2024) - not limited to safety-critical domains. First, we indicate the importance of formal methods thinking in CS education (Dongol et al., 2024), since this provides the necessary rigor in reasoning about software, its specification, its verification, and its correctness - all fundamental skills for future software developers. Then, we argue that every computer scientist needs to know formal methods (Broy et al., 2024), since the skills and knowledge acquired in this way provide the indispensable solid foundation that forms the backbone of CS practice. Finally, we underline that teaching formal methods need not come at the cost of displacing other engineering aspects of CS that are already widely accepted as essential. On the contrary, formal methods have the potential to support and strengthen the presentation and knowledge in all these subdisciplines. We provide suggestions for educators on how to incorporate formal methods into CS education.Source: ACM INROADS, vol. 15 (issue 4), pp. 58-66
DOI: 10.1145/3702231
Metrics:
See at:
IRIS Cnr | ACM Inroads | IRIS Cnr | ACM Inroads | CNR IRIS
2024
Journal article
Open Access
Evaluating the understandability and user acceptance of Attack-Defense Trees: original experiment and replication
Broccia G., Ter Beek M. H., Lluch Lafuente A., Spoletini P., Fantechi A., Ferrari A.
Context: Attack-Defense Trees (ADTs) are a graphical notation used to model and evaluate security requirements. ADTs are popular because they facilitate communication among different stakeholders involved in system security evaluation and are formal enough to be verified using methods like model checking. The understandability and user-friendliness of ADTs are claimed as key factors in their success, but these aspects, along with user acceptance, have not been evaluated empirically. Objectives: This paper presents an experiment with 25 subjects designed to assess the understandability and user acceptance of the ADT notation, along with an internal replication involving 49 subjects. Methods: The experiments adapt the Method Evaluation Model (MEM) to examine understandability variables (i.e., effectiveness and efficiency in using ADTs) and user acceptance variables (i.e., ease of use, usefulness, and intention to use). The MEM is also used to evaluate the relationships between these dimensions. In addition, a comparative analysis of the results of the two experiments is carried out. Results: With some minor differences, the outcomes of the two experiments are aligned. The results demonstrate that ADTs are well understood by participants, with values of understandability variables significantly above established thresholds. They are also highly appreciated, particularly for their ease of use. The results also show that users who are more effective in using the notation tend to evaluate it better in terms of usefulness. Conclusion: These studies provide empirical evidence supporting both the understandability and perceived acceptance of ADTs, thus encouraging further adoption of the notation in industrial contexts, and development of supporting tools.Source: INFORMATION AND SOFTWARE TECHNOLOGY, vol. 178
DOI: 10.1016/j.infsof.2024.107624
Project(s): CODECS, Secure Internet of Things – Risk analysis in design and operation, Security-by-Design in Digital Denmark, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Broccia G., Ter Beek M. H., Lluch Lafuente A., Spoletini P., Fantechi A., Ferrari A.
Context: Attack-Defense Trees (ADTs) are a graphical notation used to model and evaluate security requirements. ADTs are popular because they facilitate communication among different stakeholders involved in system security evaluation and are formal enough to be verified using methods like model checking. The understandability and user-friendliness of ADTs are claimed as key factors in their success, but these aspects, along with user acceptance, have not been evaluated empirically. Objectives: This paper presents an experiment with 25 subjects designed to assess the understandability and user acceptance of the ADT notation, along with an internal replication involving 49 subjects. Methods: The experiments adapt the Method Evaluation Model (MEM) to examine understandability variables (i.e., effectiveness and efficiency in using ADTs) and user acceptance variables (i.e., ease of use, usefulness, and intention to use). The MEM is also used to evaluate the relationships between these dimensions. In addition, a comparative analysis of the results of the two experiments is carried out. Results: With some minor differences, the outcomes of the two experiments are aligned. The results demonstrate that ADTs are well understood by participants, with values of understandability variables significantly above established thresholds. They are also highly appreciated, particularly for their ease of use. The results also show that users who are more effective in using the notation tend to evaluate it better in terms of usefulness. Conclusion: These studies provide empirical evidence supporting both the understandability and perceived acceptance of ADTs, thus encouraging further adoption of the notation in industrial contexts, and development of supporting tools.Source: INFORMATION AND SOFTWARE TECHNOLOGY, vol. 178
DOI: 10.1016/j.infsof.2024.107624
Project(s): CODECS
, Secure Internet of Things – Risk analysis in design and operation, Security-by-Design in Digital Denmark, Typeful Language Adaptation for Dynamic, Interacting and Evolving SystemsMetrics:
See at:
Information and Software Technology | IRIS Cnr | IRIS Cnr | CNR IRIS
2024
Journal article
Open Access
A configurable software model of a self-adaptive robotic system
Päßler J., Ter Beek M. H., Damiani F., Johnsen E. B., Tapia Tarifa S. L.
Self-adaptation, meant to increase reliability, is a crucial feature of cyber-physical systems operating in uncertain physical environments. Ensuring safety properties of self-adaptive systems is of utter importance, especially when operating in remote environments where communication with a human operator is limited, like under water or in space. This paper presents a software model that allows the analysis of one such self-adaptive system, a configurable underwater robot used for pipeline inspection, by means of the probabilistic model checker ProFeat. Furthermore, it shows that the configurable software model is easily extensible to further, possibly more complex use cases and analyses.Source: SCIENCE OF COMPUTER PROGRAMMING, vol. 240
DOI: 10.1016/j.scico.2024.103221
Project(s): Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Päßler J., Ter Beek M. H., Damiani F., Johnsen E. B., Tapia Tarifa S. L.
Self-adaptation, meant to increase reliability, is a crucial feature of cyber-physical systems operating in uncertain physical environments. Ensuring safety properties of self-adaptive systems is of utter importance, especially when operating in remote environments where communication with a human operator is limited, like under water or in space. This paper presents a software model that allows the analysis of one such self-adaptive system, a configurable underwater robot used for pipeline inspection, by means of the probabilistic model checker ProFeat. Furthermore, it shows that the configurable software model is easily extensible to further, possibly more complex use cases and analyses.Source: SCIENCE OF COMPUTER PROGRAMMING, vol. 240
DOI: 10.1016/j.scico.2024.103221
Project(s): Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
See at:
Science of Computer Programming | IRIS Cnr | IRIS Cnr | CNR IRIS
2024
Conference article
Open Access
Team automata: overview and roadmap
Ter Beek M. H., Hennicker R., Proença J.
Team Automata is a formalism for interacting component-based systems proposed in 1997, whereby multiple sending and receiving actions from concurrent automata can synchronise. During the past 25+ years, team automata have been studied and applied in many different contexts, involving 25+ researchers and resulting in 25+ publications. In this paper, we first revisit the specific notion of synchronisation and composition of team automata, relating it to other relevant coordination models, such as Reo, BIP, Contract Automata, Choreography Automata, and Multi-Party Session Types. We then identify several aspects that have recently been investigated for team automata and related models. These include communication properties (which are the properties of interest?), realisability (how to decompose a global model into local components?) and tool support (what has been automatised or implemented?). Our presentation of these aspects provides a snapshot of the most recent trends in research on team automata, and delineates a roadmap for future research, both for team automata and for related formalisms.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14676, pp. 161-198. Groningen, The Netherlands, 17-21/06/2024
DOI: 10.1007/978-3-031-62697-5_10
Project(s): Formal Methods in Software Engineering 2.0, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Ter Beek M. H., Hennicker R., Proença J.
Team Automata is a formalism for interacting component-based systems proposed in 1997, whereby multiple sending and receiving actions from concurrent automata can synchronise. During the past 25+ years, team automata have been studied and applied in many different contexts, involving 25+ researchers and resulting in 25+ publications. In this paper, we first revisit the specific notion of synchronisation and composition of team automata, relating it to other relevant coordination models, such as Reo, BIP, Contract Automata, Choreography Automata, and Multi-Party Session Types. We then identify several aspects that have recently been investigated for team automata and related models. These include communication properties (which are the properties of interest?), realisability (how to decompose a global model into local components?) and tool support (what has been automatised or implemented?). Our presentation of these aspects provides a snapshot of the most recent trends in research on team automata, and delineates a roadmap for future research, both for team automata and for related formalisms.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14676, pp. 161-198. Groningen, The Netherlands, 17-21/06/2024
DOI: 10.1007/978-3-031-62697-5_10
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 | doi.org | CNR IRIS | CNR IRIS
2024
Conference article
Open Access
Can AI help with the formalization of railway cybersecurity requirements?
Ter Beek M. H., Fantechi A., Gnesi S., Lenzini G., Petrocchi M.
Driven by and dependent on ICT, like almost everything today, railway transportation has become a critical infrastructure and, as such, is exposed to threats against communication of on-board and wayside components. The shift to cybersecurity brings up the need to comply with new security requirements, and once more security software engineers are confronted with a well-known problem: how to express informal requirements into unambiguous formal expressions that can be translated into enforceable policies or be used to verify the security of a system design. We have experience in translating natural language requirements from standards, regulations, and guidelines into Controlled Natural Language for Data Sharing Agreements (CNL4DSA), a formalism that serves the purpose of bridging natural and formal expressions. The translation of requirements is challenging, calling for a rigorous process of coding agreement between researchers. Following the trend of the time, in this paper, we question whether AI and, in particular, the novel Generative Language Models, can help us with this translation exercise. Previous work shows that AI can help in writing security code, although not always producing secure code; less studied is the quality of generative AI’s working with controlled natural languages in writing requirements for security compliance. Can AI be a valuable tool or companion in this endeavour too? To answer this question, we engage ChatGPT and Microsoft 365 Copilot with the same challenges that we faced when translating cybersecurity requirements for railway systems into CNL4DSA. Comparing our results from some time ago with those of the machine, we found surprising insights, showing the high potentiality of using AI in requirements engineering.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15219, pp. 186-203. Crete, Greece, 27-31/10/2024
DOI: 10.1007/978-3-031-73709-1_12
Metrics:
Ter Beek M. H., Fantechi A., Gnesi S., Lenzini G., Petrocchi M.
Driven by and dependent on ICT, like almost everything today, railway transportation has become a critical infrastructure and, as such, is exposed to threats against communication of on-board and wayside components. The shift to cybersecurity brings up the need to comply with new security requirements, and once more security software engineers are confronted with a well-known problem: how to express informal requirements into unambiguous formal expressions that can be translated into enforceable policies or be used to verify the security of a system design. We have experience in translating natural language requirements from standards, regulations, and guidelines into Controlled Natural Language for Data Sharing Agreements (CNL4DSA), a formalism that serves the purpose of bridging natural and formal expressions. The translation of requirements is challenging, calling for a rigorous process of coding agreement between researchers. Following the trend of the time, in this paper, we question whether AI and, in particular, the novel Generative Language Models, can help us with this translation exercise. Previous work shows that AI can help in writing security code, although not always producing secure code; less studied is the quality of generative AI’s working with controlled natural languages in writing requirements for security compliance. Can AI be a valuable tool or companion in this endeavour too? To answer this question, we engage ChatGPT and Microsoft 365 Copilot with the same challenges that we faced when translating cybersecurity requirements for railway systems into CNL4DSA. Comparing our results from some time ago with those of the machine, we found surprising insights, showing the high potentiality of using AI in requirements engineering.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15219, pp. 186-203. Crete, Greece, 27-31/10/2024
DOI: 10.1007/978-3-031-73709-1_12
Metrics:
See at:
IRIS Cnr | IRIS Cnr | IRIS Cnr | doi.org | CNR IRIS | CNR IRIS
2024
Contribution to book
Open Access
Formal methods for industrial critical systems: 30 years of railway applications
Ter Beek M. H., Fantechi A., Gnesi S.
This paper, written in honour of Tiziana Margaria, aims to provide a comprehensive presentation of where mainstream formal methods are currently used for modelling and analysis of railway applications.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15240, pp. 327-344
DOI: 10.1007/978-3-031-73887-6_21
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
Ter Beek M. H., Fantechi A., Gnesi S.
This paper, written in honour of Tiziana Margaria, aims to provide a comprehensive presentation of where mainstream formal methods are currently used for modelling and analysis of railway applications.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15240, pp. 327-344
DOI: 10.1007/978-3-031-73887-6_21
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Sustainable Mobility National Research Center
Metrics:
See at:
IRIS Cnr | IRIS Cnr | IRIS Cnr | doi.org | CNR IRIS | CNR IRIS
2024
Journal article
Open Access
Coherent modal transition systems refinement
Basile Davide, Ter Beek Maurice H., Fantechi Alessandro, Gnesi Stefania
Modal Transition Systems (MTS) are a well-known formalism that extend Labelled Transition Systems (LTS) with the possibility of specifying necessary and permitted behaviour. Coherent MTS (CMTS) have been introduced to model Software Product Lines (SPL) based on a correspondence between the necessary and permitted modalities of MTS transitions and their associated actions, and the core and optional features of SPL. In this paper, we address open problems of the coherent fragment of MTS and introduce the notions of refinement and thorough refinement of CMTS. Most notably, we prove that refinement and thorough refinement coincide for CMTS, while it is known that this is not the case for MTS. We also define (thorough) equivalence and strong bisimilarity of both MTS and CMTS. We show their relations and, in particular, we prove that also strong bisimilarity and equivalence coincide for CMTS, whereas they do not for MTS. Finally, we extend our investigation to CMTS equipped with Constraints (MTSC), originally introduced to express alternative behaviour, and we prove that novel notions of refinement and strong thorough refinement coincide for MTSC, and so do their extensions to strong (thorough) equivalence and strong bisimilarity.Source: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, vol. 138
DOI: 10.1016/j.jlamp.2024.100954
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Formal Methods in Software Engineering 2.0, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
Basile Davide, Ter Beek Maurice H., Fantechi Alessandro, Gnesi Stefania
Modal Transition Systems (MTS) are a well-known formalism that extend Labelled Transition Systems (LTS) with the possibility of specifying necessary and permitted behaviour. Coherent MTS (CMTS) have been introduced to model Software Product Lines (SPL) based on a correspondence between the necessary and permitted modalities of MTS transitions and their associated actions, and the core and optional features of SPL. In this paper, we address open problems of the coherent fragment of MTS and introduce the notions of refinement and thorough refinement of CMTS. Most notably, we prove that refinement and thorough refinement coincide for CMTS, while it is known that this is not the case for MTS. We also define (thorough) equivalence and strong bisimilarity of both MTS and CMTS. We show their relations and, in particular, we prove that also strong bisimilarity and equivalence coincide for CMTS, whereas they do not for MTS. Finally, we extend our investigation to CMTS equipped with Constraints (MTSC), originally introduced to express alternative behaviour, and we prove that novel notions of refinement and strong thorough refinement coincide for MTSC, and so do their extensions to strong (thorough) equivalence and strong bisimilarity.Source: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, vol. 138
DOI: 10.1016/j.jlamp.2024.100954
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms, Formal Methods in Software Engineering 2.0, Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems
Metrics:
See at:
Journal of Logical and Algebraic Methods in Programming | IRIS Cnr | IRIS Cnr | CNR IRIS
2024
Journal article
Open Access
Advanced integrated evaluation of railway systems
Davide Basile, Maurice Ter Beek, Felicita Di Giandomenico, Laura Carnevali, Alessandro Fantechi
Researchers from the Software Technologies Lab (STLAB) of the University of Florence and the two research labs Formal Methods and Tools (FMT) and Software Engineering and Dependable Computing (SEDC) of CNR-ISTI join forces to work on innovative solutions for the evaluation of railway systems. The research is conducted in the context of the national project ADVENTURE funded by the Italian Ministry for Universities and Research (MUR) under the program for Projects of National Interest (PRIN).Source: ERCIM NEWS, pp. 53-54
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms
Davide Basile, Maurice Ter Beek, Felicita Di Giandomenico, Laura Carnevali, Alessandro Fantechi
Researchers from the Software Technologies Lab (STLAB) of the University of Florence and the two research labs Formal Methods and Tools (FMT) and Software Engineering and Dependable Computing (SEDC) of CNR-ISTI join forces to work on innovative solutions for the evaluation of railway systems. The research is conducted in the context of the national project ADVENTURE funded by the Italian Ministry for Universities and Research (MUR) under the program for Projects of National Interest (PRIN).Source: ERCIM NEWS, pp. 53-54
Project(s): ADVancEd iNtegraTed evalUation of Railway systEms
See at:
ercim-news.ercim.eu | CNR IRIS | CNR IRIS