2024
Journal article
Open Access
Product lines of dataflows
Lienhardt M., Ter Beek M. H., 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 210 (2024). doi:10.1016/j.jss.2023.111928
DOI: 10.1016/j.jss.2023.111928
Metrics:
Lienhardt M., Ter Beek M. H., 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 210 (2024). doi:10.1016/j.jss.2023.111928
DOI: 10.1016/j.jss.2023.111928
Metrics:
See at:
ISTI Repository 
| ISTI Repository | www.sciencedirect.com | CNR ExploRA
2023
Contribution to journal
Open Access
Systems and software product lines of the future
Ter Beek M. H., Schaefer I.
Source: The Journal of systems and software 199 (2023). doi:10.1016/j.jss.2023.111622
DOI: 10.1016/j.jss.2023.111622
Metrics:
Ter Beek M. H., Schaefer I.
Source: The Journal of systems and software 199 (2023). doi:10.1016/j.jss.2023.111622
DOI: 10.1016/j.jss.2023.111622
Metrics:
See at:
ISTI Repository | www.sciencedirect.com 
| CNR ExploRA
2023
Conference article
Open Access
Can we communicate? Using dynamic logic to verify team automata
Ter Beek M. H., Cledou G., Hennicker R., Proença J.
Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Given such a team automaton, we can reason over communication properties such as receptiveness (sent messages must be received) and responsiveness (pending receivesmust be satisfied). Previouswork focused on how to identify these communication properties. However, automatically verifying these properties is non-trivial, as it may involve traversing networks of interacting automata with large state spaces. This paper investigates (1) how to characterise communication properties for team automata (and subsumed models) using test-free propositional dynamic logic, and (2) how to use this characterisation to verify communication properties by model checking. A prototype tool supports the theory, using a transformation to interact with the mCRL2 tool for model checking.Source: FM'23 - 25th International Symposium on Formal Methods, pp. 122–141, Lübeck, Germany, 6-10/3/2023
DOI: 10.1007/978-3-031-27481-7_9
Metrics:
Ter Beek M. H., Cledou G., Hennicker R., Proença J.
Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Given such a team automaton, we can reason over communication properties such as receptiveness (sent messages must be received) and responsiveness (pending receivesmust be satisfied). Previouswork focused on how to identify these communication properties. However, automatically verifying these properties is non-trivial, as it may involve traversing networks of interacting automata with large state spaces. This paper investigates (1) how to characterise communication properties for team automata (and subsumed models) using test-free propositional dynamic logic, and (2) how to use this characterisation to verify communication properties by model checking. A prototype tool supports the theory, using a transformation to interact with the mCRL2 tool for model checking.Source: FM'23 - 25th International Symposium on Formal Methods, pp. 122–141, Lübeck, Germany, 6-10/3/2023
DOI: 10.1007/978-3-031-27481-7_9
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2023
Conference article
Open Access
A runtime environment for contract automata
Basile D., Ter Beek M. H.
Contract automata have been introduced for specifying applications through behavioural contracts and for synthesising their orchestrations as finite state automata. This paper addresses the realisation of applications from contract automata specifications. We present CARE, a new runtime environment to coordinate services implementing contracts that guarantees the adherence of the implementation to its contract. We discuss how CARE can be adopted to realise contract-based applications, its formal guarantees, and we identify the responsibilities of the involved business actors. Experiments show the benefits of adopting CARE with respect to manual implementations.Source: FM'23 - 25th International Symposium on Formal Methods, pp. 550–567, Lübeck, Germany, 6-10/3/2023
DOI: 10.1007/978-3-031-27481-7_31
Metrics:
Basile D., Ter Beek M. H.
Contract automata have been introduced for specifying applications through behavioural contracts and for synthesising their orchestrations as finite state automata. This paper addresses the realisation of applications from contract automata specifications. We present CARE, a new runtime environment to coordinate services implementing contracts that guarantees the adherence of the implementation to its contract. We discuss how CARE can be adopted to realise contract-based applications, its formal guarantees, and we identify the responsibilities of the involved business actors. Experiments show the benefits of adopting CARE with respect to manual implementations.Source: FM'23 - 25th International Symposium on Formal Methods, pp. 550–567, Lübeck, Germany, 6-10/3/2023
DOI: 10.1007/978-3-031-27481-7_31
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2023
Conference article
Open Access
Mutant equivalence as monotonicity in parametric timed games
Basile D., Ter Beek M. H., Göttmann H., Lochau M.
The detection of faults in software systems can be enhanced effectively by model-based mutation testing. The efficiency of this technique is hindered when mutants are equivalent to the original system model, since this makes them useless. Recently, the application of model-based mutation testing to real-time systems modelled as timed games has been investigated, which has resulted in guidelines for statically avoiding equivalent mutants. In this paper, we recast this problem into the framework of parametric timed games. We then prove a correspondence between theoretical results for the detection of equivalent mutants in timed games and the property of monotonicity that is known to hold for a sub-class of parametric timed games called L/U parametric timed games. The presented results not only simplify the theory underlying the detection of equivalent mutants in timed games, but at the same time they improve the expressiveness of a known decidable fragment of parametric timed games for which monotonicity holds.Source: FormaliSE'23 - 11th IEEE/ACM International Conference on Formal Methods in Software Engineering, pp. 55–65, Melbourne, Australia, 14-15/05/2023
DOI: 10.1109/formalise58978.2023.00014
Metrics:
Basile D., Ter Beek M. H., Göttmann H., Lochau M.
The detection of faults in software systems can be enhanced effectively by model-based mutation testing. The efficiency of this technique is hindered when mutants are equivalent to the original system model, since this makes them useless. Recently, the application of model-based mutation testing to real-time systems modelled as timed games has been investigated, which has resulted in guidelines for statically avoiding equivalent mutants. In this paper, we recast this problem into the framework of parametric timed games. We then prove a correspondence between theoretical results for the detection of equivalent mutants in timed games and the property of monotonicity that is known to hold for a sub-class of parametric timed games called L/U parametric timed games. The presented results not only simplify the theory underlying the detection of equivalent mutants in timed games, but at the same time they improve the expressiveness of a known decidable fragment of parametric timed games for which monotonicity holds.Source: FormaliSE'23 - 11th IEEE/ACM International Conference on Formal Methods in Software Engineering, pp. 55–65, Melbourne, Australia, 14-15/05/2023
DOI: 10.1109/formalise58978.2023.00014
Metrics:
See at:
ISTI Repository | ieeexplore.ieee.org | CNR ExploRA
2023
Conference article
Open Access
Evaluating a language workbench: from working memory capacity to comprehension to acceptance
Broccia G., Ferrari A., Ter Beek M. H., Cazzola W., Favalli L., Bertolotti F.
Language workbenches are tools that enable the definition, reuse and composition of programming languages and their ecosystem. This breed of frameworks aims to make the development of new languages easier and more affordable. Consequently, the comprehensibility of the language used in a language workbench (i.e., the meta-language) should be an important aspect to consider and evaluate. To the best of our knowledge, although the quantitative aspects of language workbenches are often discussed in the literature, the evaluation of comprehensibility is typically neglected. Neverlang is a language workbench that enables the definition of languages with a modular approach. This paper presents a preliminary study that intends to assess the comprehensibility of Neverlang programs, evaluated in terms of users' effectiveness and efficiency in a code comprehension task. The study also investigates the relationship between Neverlang comprehensibility and the users' working memory capacity. Furthermore, we intend to capture the relationship between Neverlang comprehensibility and users' acceptance, in terms of perceived ease of use, perceived usefulness, and intention to use. Our preliminary results on 10 subjects suggest that the users' working memory capacity may be related to the ability to comprehend Neverlang programs. On the other hand, effectiveness and efficiency do not appear to be associated with an increase in users' acceptance variables.Source: ICPC'23 - 31st IEEE/ACM International Conference on Program Comprehension, pp. 54–58, Melbourne, Australia, 15-16/05/2023
DOI: 10.1109/icpc58990.2023.00017
Metrics:
Broccia G., Ferrari A., Ter Beek M. H., Cazzola W., Favalli L., Bertolotti F.
Language workbenches are tools that enable the definition, reuse and composition of programming languages and their ecosystem. This breed of frameworks aims to make the development of new languages easier and more affordable. Consequently, the comprehensibility of the language used in a language workbench (i.e., the meta-language) should be an important aspect to consider and evaluate. To the best of our knowledge, although the quantitative aspects of language workbenches are often discussed in the literature, the evaluation of comprehensibility is typically neglected. Neverlang is a language workbench that enables the definition of languages with a modular approach. This paper presents a preliminary study that intends to assess the comprehensibility of Neverlang programs, evaluated in terms of users' effectiveness and efficiency in a code comprehension task. The study also investigates the relationship between Neverlang comprehensibility and the users' working memory capacity. Furthermore, we intend to capture the relationship between Neverlang comprehensibility and users' acceptance, in terms of perceived ease of use, perceived usefulness, and intention to use. Our preliminary results on 10 subjects suggest that the users' working memory capacity may be related to the ability to comprehend Neverlang programs. On the other hand, effectiveness and efficiency do not appear to be associated with an increase in users' acceptance variables.Source: ICPC'23 - 31st IEEE/ACM International Conference on Program Comprehension, pp. 54–58, Melbourne, Australia, 15-16/05/2023
DOI: 10.1109/icpc58990.2023.00017
Metrics:
See at:
ISTI Repository | ieeexplore.ieee.org | CNR ExploRA
2023
Conference article
Open Access
Research challenges in orchestration synthesis
Basile D., Ter Beek M. H.
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 fact, the resulting orchestration is such that as much of the behaviour in agreement is maintained. In this paper, we discuss recent developments of the orchestration synthesis algorithm for contract automata. Notably, we present a refined notion of semi-controllability and compare it with the original notion by means of examples. We then discuss the current limits of the orchestration synthesis algorithm and identify a number of research challenges together with a research roadmap.Source: ICE 2023 - 16th Interaction and Concurrency Experience, Lisbon, Portugal, 19/6/2023
DOI: 10.4204/eptcs.383.5
Metrics:
Basile D., Ter Beek M. H.
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 fact, the resulting orchestration is such that as much of the behaviour in agreement is maintained. In this paper, we discuss recent developments of the orchestration synthesis algorithm for contract automata. Notably, we present a refined notion of semi-controllability and compare it with the original notion by means of examples. We then discuss the current limits of the orchestration synthesis algorithm and identify a number of research challenges together with a research roadmap.Source: ICE 2023 - 16th Interaction and Concurrency Experience, Lisbon, Portugal, 19/6/2023
DOI: 10.4204/eptcs.383.5
Metrics:
See at:
cgi.cse.unsw.edu.au | ISTI Repository | CNR ExploRA
2023
Software
Unknown
A toolchain for strategy synthesis with spatial properties - Complementary material
Basile D., Ter Beek M. H., Bussi L., Ciancia V.
This is the complementary material for our paper ``A Toolchain for Strategy Synthesis with Spatial Properties'' accepted for publication at the Journal of Software Tools and Technology Transfer. This repository contains a permanent snapshot of https://github.com/contractautomataproject/CATLib_PngConverter/tree/ec0938043146b008bbbcb4ed3ec79c06dd2e47d6DOI: 10.5281/zenodo.8220527
Metrics:
Basile D., Ter Beek M. H., Bussi L., Ciancia V.
This is the complementary material for our paper ``A Toolchain for Strategy Synthesis with Spatial Properties'' accepted for publication at the Journal of Software Tools and Technology Transfer. This repository contains a permanent snapshot of https://github.com/contractautomataproject/CATLib_PngConverter/tree/ec0938043146b008bbbcb4ed3ec79c06dd2e47d6DOI: 10.5281/zenodo.8220527
Metrics:
See at: CNR ExploRA
2023
Contribution to conference
Open Access
27th ACM International Systems and Software Product Line Conference (SPLC 2023). Proceedings - Volume A
Arcaini P., Ter Beek M. H., Perrouin G., Reinhartz-Berger I., Luaces M. R., Schwanninger C., Ali S., Varshosaz M., Gargantini A., Gnesi S., Lochau M., Semini L., Washizaki H.
Welcome to SPLC'23, the 27th ACM International Systems and Software Product Line Conference. Looking back to the previous SPLC issues, the conference has been established as 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'23 acted as a venue fostering knowledge exchange and learning about the state of the art in software product lines aswell as newpractices, trends, innovations, insights from industrial applications, and new challenges. SPLC'23 was held at Hitotsubashi Hall in Tokyo, Japan, from August 28 to September 1, 2023.Source: New York: ACM Press, 2023
DOI: 10.1145/3579027
Metrics:
Arcaini P., Ter Beek M. H., Perrouin G., Reinhartz-Berger I., Luaces M. R., Schwanninger C., Ali S., Varshosaz M., Gargantini A., Gnesi S., Lochau M., Semini L., Washizaki H.
Welcome to SPLC'23, the 27th ACM International Systems and Software Product Line Conference. Looking back to the previous SPLC issues, the conference has been established as 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'23 acted as a venue fostering knowledge exchange and learning about the state of the art in software product lines aswell as newpractices, trends, innovations, insights from industrial applications, and new challenges. SPLC'23 was held at Hitotsubashi Hall in Tokyo, Japan, from August 28 to September 1, 2023.Source: New York: ACM Press, 2023
DOI: 10.1145/3579027
Metrics:
See at:
dl.acm.org | ISTI Repository | CNR ExploRA
2023
Contribution to conference
Open Access
27th ACM International Systems and Software Product Line Conference (SPLC 2023). Proceedings - Volume B
Arcaini P., Ter Beek M. H., Perrouin G., Reinhartz-Berger I., Machado I., Vergilio S. R., Rabiser R., Yue T., Devroey X., Pinto M., Washizaki H.
Welcome to SPLC'23, the 27th ACM International Systems and Software Product Line Conference. Looking back to the previous SPLC issues, the conference has been established as 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'23 acted as a venue fostering knowledge exchange and learning about the state of the art in software product lines aswell as newpractices, trends, innovations, insights from industrial applications, and new challenges. SPLC'23 was held at Hitotsubashi Hall in Tokyo, Japan, from August 28 to September 1, 2023.Source: New York: ACM Press, 2023
DOI: 10.1145/3579028
Metrics:
Arcaini P., Ter Beek M. H., Perrouin G., Reinhartz-Berger I., Machado I., Vergilio S. R., Rabiser R., Yue T., Devroey X., Pinto M., Washizaki H.
Welcome to SPLC'23, the 27th ACM International Systems and Software Product Line Conference. Looking back to the previous SPLC issues, the conference has been established as 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'23 acted as a venue fostering knowledge exchange and learning about the state of the art in software product lines aswell as newpractices, trends, innovations, insights from industrial applications, and new challenges. SPLC'23 was held at Hitotsubashi Hall in Tokyo, Japan, from August 28 to September 1, 2023.Source: New York: ACM Press, 2023
DOI: 10.1145/3579028
Metrics:
See at:
dl.acm.org | ISTI Repository | CNR ExploRA
2023
Report
Open Access
Formal modelling and analysis of a self-adaptive robotic system
Päßler J., Ter Beek M. H., Damiani F., Tapia Tarifa S. L., Johnsen E. B.
Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems are often modelled 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 a self-adaptive robotic system; more concretely, an autonomous underwater vehicle (AUV) used for pipeline inspection. In this paper, we model and analyse it with the feature-aware probabilistic model checker ProFeat. The functionalities of the AUV are modelled in a feature model, capturing the AUV's variability. This allows us to model the managed subsystem of the AUV as a family of systems, where each family member corresponds to a valid feature configuration of the AUV. The managing subsystem of the AUV is modelled as a control layer capable of dynamically switching between such valid feature configurations, depending both on environmental and internal conditions. We use this model to analyse probabilistic reward and safety properties for the AUV.Source: ISTI Technical Report, ISTI-2023-TR/008, pp.1–18, 2023
DOI: 10.32079/isti-tr-2023/008
Metrics:
Päßler J., Ter Beek M. H., Damiani F., Tapia Tarifa S. L., Johnsen E. B.
Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems are often modelled 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 a self-adaptive robotic system; more concretely, an autonomous underwater vehicle (AUV) used for pipeline inspection. In this paper, we model and analyse it with the feature-aware probabilistic model checker ProFeat. The functionalities of the AUV are modelled in a feature model, capturing the AUV's variability. This allows us to model the managed subsystem of the AUV as a family of systems, where each family member corresponds to a valid feature configuration of the AUV. The managing subsystem of the AUV is modelled as a control layer capable of dynamically switching between such valid feature configurations, depending both on environmental and internal conditions. We use this model to analyse probabilistic reward and safety properties for the AUV.Source: ISTI Technical Report, ISTI-2023-TR/008, pp.1–18, 2023
DOI: 10.32079/isti-tr-2023/008
Metrics:
See at: CNR ExploRA
2023
Contribution to journal
Open Access
Introduction to the special collection from iFM 2022
Monahan R., Ter Beek M. H.
Source: Formal aspects of computing 35 (2023): 1–2. doi:10.1145/3622995
DOI: 10.1145/3622995
Metrics:
Monahan R., Ter Beek M. H.
Source: Formal aspects of computing 35 (2023): 1–2. doi:10.1145/3622995
DOI: 10.1145/3622995
Metrics:
See at:
dl.acm.org | ISTI Repository | CNR ExploRA
2023
Journal article
Open Access
A toolchain for strategy synthesis with spatial properties
Basile D., Ter Beek M. H, Bussi L., Ciancia V.
We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools \texttt{CATLib} and \texttt{VoxLogicA} to interact in a fully automated way. The Contract Automata Library (\texttt{CATLib}) is aimed at both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (\texttt{VoxLogicA}) is a spatial model checker for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain. The strategies are synthesised with \texttt{CAT\-Lib}, while the properties to enforce are defined by means of spatial model checking of the images with \texttt{VoxLogicA}. The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems. We discuss the toolchain's performance also considering several recent improvements.Source: International journal on software tools for technology transfer (Print) 25 (2023): 641–658. doi:10.1007/s10009-023-00730-1
DOI: 10.1007/s10009-023-00730-1
Metrics:
Basile D., Ter Beek M. H, Bussi L., Ciancia V.
We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools \texttt{CATLib} and \texttt{VoxLogicA} to interact in a fully automated way. The Contract Automata Library (\texttt{CATLib}) is aimed at both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (\texttt{VoxLogicA}) is a spatial model checker for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain. The strategies are synthesised with \texttt{CAT\-Lib}, while the properties to enforce are defined by means of spatial model checking of the images with \texttt{VoxLogicA}. The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems. We discuss the toolchain's performance also considering several recent improvements.Source: International journal on software tools for technology transfer (Print) 25 (2023): 641–658. doi:10.1007/s10009-023-00730-1
DOI: 10.1007/s10009-023-00730-1
Metrics:
See at:
ISTI Repository | ISTI Repository | CNR ExploRA
2023
Contribution to conference
Open Access
Preface. Proceedings of the First Workshop on Trends in Configurable Systems Analysis (TiCSA'23)
Ter Beek M. H., Dubslaff C.
The analysis of configurable systems, i.e., systems those behaviors depend on parameters or support various features, is challenging due to the exponential blowup arising in the number of configuration options. This volume contains the post-proceedings of TiCSA 2023, the first workshop on Trends in Configurable Systems Analysis, where current challenges and solutions in configurable systems analysis were presented and discussed.DOI: 10.4204/eptcs.392
Metrics:
Ter Beek M. H., Dubslaff C.
The analysis of configurable systems, i.e., systems those behaviors depend on parameters or support various features, is challenging due to the exponential blowup arising in the number of configuration options. This volume contains the post-proceedings of TiCSA 2023, the first workshop on Trends in Configurable Systems Analysis, where current challenges and solutions in configurable systems analysis were presented and discussed.DOI: 10.4204/eptcs.392
Metrics:
See at:
cgi.cse.unsw.edu.au | CNR ExploRA
2023
Conference article
Open Access
Formal modelling and analysis of a self-adaptive robotic system
Päßler J., Ter Beek M. H., Damiani F., Tapia Tarifa S. L., Johnsen E. B.
Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems are often modelled 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 a self-adaptive robotic system; more concretely, an autonomous underwater vehicle (AUV) used for pipeline inspection. In this paper, we model and analyse it with the feature-aware probabilistic model checker ProFeat. The functionalities of the AUV are modelled in a feature model, capturing the AUV's variability. This allows us to model the managed subsystem of the AUV as a family of systems, where each family member corresponds to a valid feature configuration of the AUV. The managing subsystem of the AUV is modelled as a control layer capable of dynamically switching between such valid feature configurations, depending both on environmental and internal conditions. We use this model to analyse probabilistic reward and safety properties for the AUV.Source: iFM'23 - 18th International Conference on integrated Formal Methods, pp. 343–363, Leiden, The Netherlands, 13-15/11/2023
DOI: 10.1007/978-3-031-47705-8_18
Metrics:
Päßler J., Ter Beek M. H., Damiani F., Tapia Tarifa S. L., Johnsen E. B.
Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems are often modelled 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 a self-adaptive robotic system; more concretely, an autonomous underwater vehicle (AUV) used for pipeline inspection. In this paper, we model and analyse it with the feature-aware probabilistic model checker ProFeat. The functionalities of the AUV are modelled in a feature model, capturing the AUV's variability. This allows us to model the managed subsystem of the AUV as a family of systems, where each family member corresponds to a valid feature configuration of the AUV. The managing subsystem of the AUV is modelled as a control layer capable of dynamically switching between such valid feature configurations, depending both on environmental and internal conditions. We use this model to analyse probabilistic reward and safety properties for the AUV.Source: iFM'23 - 18th International Conference on integrated Formal Methods, pp. 343–363, Leiden, The Netherlands, 13-15/11/2023
DOI: 10.1007/978-3-031-47705-8_18
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2023
Conference article
Open Access
Realisability of global models of interaction
Ter Beek M. H., Hennicker R., Proença J.
We consider global models of communicating agents specified as transition systems labelled by interactions in which multiple senders and receivers can participate. A realisation of such a model is a set of local transition systems--one per agent--which are executed concurrently using synchronous communication. Our core challenge is how to check whether a global model is realisable and, if it is, how to synthesise a realisation. We identify and compare two variants to realise global interaction models, both relying on bisimulation equivalence. Then we investigate, for both variants, realisability conditions to be checked on global models. We propose a synthesis method for the construction of realisations by grouping locally indistinguishable states. The paper is accompanied by a tool that implements realisability checks and synthesises realisations.Source: ICTAC'23 - 20th International Colloquium on Theoretical Aspects of Computing, pp. 236–255, Lima, Perù, 4-8/12/2023
DOI: 10.1007/978-3-031-47963-2_15
Metrics:
Ter Beek M. H., Hennicker R., Proença J.
We consider global models of communicating agents specified as transition systems labelled by interactions in which multiple senders and receivers can participate. A realisation of such a model is a set of local transition systems--one per agent--which are executed concurrently using synchronous communication. Our core challenge is how to check whether a global model is realisable and, if it is, how to synthesise a realisation. We identify and compare two variants to realise global interaction models, both relying on bisimulation equivalence. Then we investigate, for both variants, realisability conditions to be checked on global models. We propose a synthesis method for the construction of realisations by grouping locally indistinguishable states. The paper is accompanied by a tool that implements realisability checks and synthesises realisations.Source: ICTAC'23 - 20th International Colloquium on Theoretical Aspects of Computing, pp. 236–255, Lima, Perù, 4-8/12/2023
DOI: 10.1007/978-3-031-47963-2_15
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2023
Contribution to journal
Open Access
Preface. Selected papers of the 24th international conference on coordination models and languages (COORDINATION 2022)
Ter Beek M. H., Sirjani M.
Source: Logical Methods in Computer Science 19 (2023).
Ter Beek M. H., Sirjani M.
Source: Logical Methods in Computer Science 19 (2023).
See at:
lmcs.episciences.org | ISTI Repository | CNR ExploRA
2022
Journal article
Open Access
Efficient static analysis and verification of featured transition systems
Ter Beek M. H., Damiani F., Lienhardt M., Mazzanti F., Paolini L.
A Featured Transition System (FTS) models the behaviour of all products of a Software Product Line (SPL) in a single compact structure, by associating action-labelled transitions with features that condition their presence in product behaviour. It may however be the case that the resulting featured transitions of an FTS cannot be executed in any product (so called dead transitions) or, on the contrary, can be executed in all products (so called false optional transitions). Moreover, an FTS may contain states from which a transition can be executed only in some products (so called hidden deadlock states). It is useful to detect such ambiguities and signal them to the modeller, because dead transitions indicate an anomaly in the FTS that must be corrected, false optional transitions indicate a redundancy that may be removed, and hidden deadlocks should be made explicit in the FTS to improve the understanding of the model and to enable efficient verification - if the deadlocks in the products should not be remedied in the first place. We provide an algorithm to analyse an FTS for ambiguities and a means to transform an ambiguous FTS into an unambiguous one. The scope is twofold: an ambiguous model is typically undesired as it gives an unclear idea of the SPL and, moreover, an unambiguous FTS can efficiently be model checked. We empirically show the suitability of the algorithm by applying it to a number of benchmark SPL examples from the literature, and we show how this facilitates a kind of family-based model checking of a wide range of properties on FTSs.Source: Empirical software engineering (Online) 27 (2022). doi:10.1007/s10664-020-09930-8
DOI: 10.1007/s10664-020-09930-8
Metrics:
Ter Beek M. H., Damiani F., Lienhardt M., Mazzanti F., Paolini L.
A Featured Transition System (FTS) models the behaviour of all products of a Software Product Line (SPL) in a single compact structure, by associating action-labelled transitions with features that condition their presence in product behaviour. It may however be the case that the resulting featured transitions of an FTS cannot be executed in any product (so called dead transitions) or, on the contrary, can be executed in all products (so called false optional transitions). Moreover, an FTS may contain states from which a transition can be executed only in some products (so called hidden deadlock states). It is useful to detect such ambiguities and signal them to the modeller, because dead transitions indicate an anomaly in the FTS that must be corrected, false optional transitions indicate a redundancy that may be removed, and hidden deadlocks should be made explicit in the FTS to improve the understanding of the model and to enable efficient verification - if the deadlocks in the products should not be remedied in the first place. We provide an algorithm to analyse an FTS for ambiguities and a means to transform an ambiguous FTS into an unambiguous one. The scope is twofold: an ambiguous model is typically undesired as it gives an unclear idea of the SPL and, moreover, an unambiguous FTS can efficiently be model checked. We empirically show the suitability of the algorithm by applying it to a number of benchmark SPL examples from the literature, and we show how this facilitates a kind of family-based model checking of a wide range of properties on FTSs.Source: Empirical software engineering (Online) 27 (2022). doi:10.1007/s10664-020-09930-8
DOI: 10.1007/s10664-020-09930-8
Metrics:
See at:
link.springer.com | ISTI Repository | ISTI Repository | CNR ExploRA
2022
Journal article
Restricted
Formal Methods in railways: a systematic mapping study
Ferrari A., Ter Beek M. H.
Formal methods are mathematically based techniques for the rigorous development of software-intensive systems. The railway signaling domain is a field in which formal methods have traditionally been applied, with several success stories. This article reports on a mapping study that surveys the landscape of research on applications of formal methods to the development of railway systems. Following the guidelines of systematic reviews, we identify 328 relevant primary studies, and extract information about their demographics, the characteristics of formal methods used and railway-specific aspects. Our main results are as follows: (i) we identify a total of 328 primary studies relevant to our scope published between 1989 and 2020, of which 44% published during the last 5 years and 24% involving industry; (ii) the majority of studies are evaluated through Examples (41%) and Experience Reports (38%), while full-fledged Case Studies are limited (1.5%); (iii) Model checking is the most commonly adopted technique (47%), followed by simulation (27%) and theorem proving (19.5%); (iv) the dominant languages are UML (18%) and B (15%), while frequently used tools are ProB (9%), NuSMV (8%) and UPPAAL (7%); however, a diverse landscape of languages and tools is employed; (v) the majority of systems are interlocking products (40%), followed by models of high-level control logic (27%); (vi) most of the studies focus on the Architecture (66%) and Detailed Design (45%) development phases. Based on these findings, we highlight current research gaps and expected actions. In particular, the need to focus on more empirically sound research methods, such as Case Studies and Controlled Experiments, and to lower the degree of abstraction, by applying formal methods and tools to development phases that are closer to software development. Our study contributes with an empirically based perspective on the future of research and practice in formal methods applications for railways. It can be used by formal methods researchers to better focus their scientific inquiries, and by railway practitioners for an improved understanding of the interplay between formal methods and their specific application domain.Source: ACM computing surveys 55 (2022). doi:10.1145/3520480
DOI: 10.1145/3520480
Project(s): 4SECURAIL
, ASTRail
Metrics:
Ferrari A., Ter Beek M. H.
Formal methods are mathematically based techniques for the rigorous development of software-intensive systems. The railway signaling domain is a field in which formal methods have traditionally been applied, with several success stories. This article reports on a mapping study that surveys the landscape of research on applications of formal methods to the development of railway systems. Following the guidelines of systematic reviews, we identify 328 relevant primary studies, and extract information about their demographics, the characteristics of formal methods used and railway-specific aspects. Our main results are as follows: (i) we identify a total of 328 primary studies relevant to our scope published between 1989 and 2020, of which 44% published during the last 5 years and 24% involving industry; (ii) the majority of studies are evaluated through Examples (41%) and Experience Reports (38%), while full-fledged Case Studies are limited (1.5%); (iii) Model checking is the most commonly adopted technique (47%), followed by simulation (27%) and theorem proving (19.5%); (iv) the dominant languages are UML (18%) and B (15%), while frequently used tools are ProB (9%), NuSMV (8%) and UPPAAL (7%); however, a diverse landscape of languages and tools is employed; (v) the majority of systems are interlocking products (40%), followed by models of high-level control logic (27%); (vi) most of the studies focus on the Architecture (66%) and Detailed Design (45%) development phases. Based on these findings, we highlight current research gaps and expected actions. In particular, the need to focus on more empirically sound research methods, such as Case Studies and Controlled Experiments, and to lower the degree of abstraction, by applying formal methods and tools to development phases that are closer to software development. Our study contributes with an empirically based perspective on the future of research and practice in formal methods applications for railways. It can be used by formal methods researchers to better focus their scientific inquiries, and by railway practitioners for an improved understanding of the interplay between formal methods and their specific application domain.Source: ACM computing surveys 55 (2022). doi:10.1145/3520480
DOI: 10.1145/3520480
Project(s): 4SECURAIL
, ASTRail Metrics:
See at:
dl.acm.org | CNR ExploRA
2022
Report
Open Access
A runtime environment for contract automata
Basile D., Ter Beek M. H.
Realising contract-based applications from formal specifications with formal guarantees requires to show the adherence of a specification, the contract, to its implementation. Contract automata have been introduced for specifying contract-based applications and synthesising their orchestrations as finite state automata. This paper introduces CARE, a newly developed library for implementing applications specified via contract automata, providing a runtime environment to coordinate services implementing contracts.Source: ISTI Working papers, pp.1–8, 2022
Basile D., Ter Beek M. H.
Realising contract-based applications from formal specifications with formal guarantees requires to show the adherence of a specification, the contract, to its implementation. Contract automata have been introduced for specifying contract-based applications and synthesising their orchestrations as finite state automata. This paper introduces CARE, a newly developed library for implementing applications specified via contract automata, providing a runtime environment to coordinate services implementing contracts.Source: ISTI Working papers, pp.1–8, 2022
See at:
arxiv.org | ISTI Repository | CNR ExploRA