246 result(s)
Page Size: 10, 20, 50
Export: bibtex, xml, json, csv
Order by:

CNR Author operator: and / or
more
Typology operator: and / or
Language operator: and / or
Date operator: and / or
more
Rights operator: and / or
2022 Journal article Open Access OPEN

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

See at: link.springer.com Open Access | ISTI Repository Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2022 Journal article Open Access OPEN

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 (2022). doi:10.1145/3520480
DOI: 10.1145/3520480
Project(s): 4SECURAIL via OpenAIRE, ASTRail via OpenAIRE

See at: dl.acm.org Open Access | CNR ExploRA Open Access


2022 Report Open Access OPEN

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

See at: arxiv.org Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2022 Journal article Open Access OPEN

Formal methods and tools for industrial critical systems
Ter Beek M. H., Larsen K. G., Nickovic D., Willemse T. A. C.
Formal methods and tools have become well established and widely applied to ensure the correctness of fundamental components of industrial critical systems in domains like railways, avionics and automotive. In this Introduction to the special issue, we outline a number of recent achievements concerning the use of formal methods and tools for the specification and verification of critical systems from a variety of industrial domains. These achievements are represented by eight properly revised and extended versions of papers that were selected from the 24th and 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2019 and FMICS 2020).Source: International journal on software tools for technology transfer (Internet) 24 (2022): 325–330. doi:10.1007/s10009-022-00660-4
DOI: 10.1007/s10009-022-00660-4

See at: ISTI Repository Open Access | link.springer.com Restricted | CNR ExploRA Restricted


2022 Journal article Open Access OPEN

Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods
Basile D., Ter Beek M. H., Ferrari A., Legay A.
Shift2Rail is a joint undertaking funded by the EU via its Horizon 2020 program and by main railway stakeholders. Several Shift2Rail projects aim to investigate the application of formal methods to new ERTMS/ETCS railway signalling systems that promise to move European railway forward by guaranteeing high capacity, low cost and improved reliability. We explore the ERTMS/ETCS level 3 full moving block specifications stemming from different Shift2Rail projects using UPPAAL and statistical model checking. The results range from novel rigorously formalised requirements to an operational model formally verified against scenarios with multiple trains on a single railway line. From the gained experience, we have distilled future research goals to improve the formal specification and verification of real-time systems, and we discuss some barriers concerning a possible uptake of formal methods and tools in the railway industrySource: International journal on software tools for technology transfer (Internet) 24 (2022): 351–370. doi:10.1007/s10009-022-00653-3
DOI: 10.1007/s10009-022-00653-3
Project(s): 4SECURAIL via OpenAIRE, ASTRail via OpenAIRE

See at: link.springer.com Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2022 Contribution to conference Open Access OPEN

Integrated Formal Methods - Proceedings of the 17th International Conference on Integrated Formal Methods (IFM'22)
M. H. Ter Beek, R. Monahan
This book constitutes the refereed proceedings of the 17th International Conference on Integrated Formal Methods, IFM 2022, held in Lugano, Switzerland, in June 2022. The 14 full papers and 2 short papers were carefully reviewed and selected from 46 submissions. The papers are categorized into the following topical sub-headings: Invited Papers; Cooperative and Relational Verification; B Method; Time; Probability; learning and Synthesis; Security; Stats Analysis and Testing; PhD Symposium Presentations.DOI: 10.1007/978-3-031-07727-2

See at: link.springer.com Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2022 Contribution to conference Open Access OPEN

Coordination Models and Languages - Proceedings of the 24th International Conference on Coordination Models and Languages (COORDINATION'22)
Ter Beek M. H., Sirjani M.
This book constitutes the refereed proceedings of the 24th IFIP WG 6.1 International Conference on Coordination Models and Language, COORDINATION 2022, held in Lucca, Italy, in June 2022, as part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022. The 11 regular papers and one short paper presented in this book were carefully reviewed and selected from 22 submissions. COORDINATION provides a well-established forum for the growing community of researchers interested in coordination models and languages, architectures, verification and implementation techniques necessary to cope with the complexity induced by the demands of today's software development.DOI: 10.1007/978-3-031-08143-9

See at: link.springer.com Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2021 Report Open Access OPEN

Quantitative security risk modeling and analysis with RisQFLan
Ter Beek M. H., Legay A., Lluch Lafuente A., Vandin A.
Domain-specific quantitative modeling and analysis approaches are fundamental in scenarios in which qualitative approaches are inappropriate or unfeasible. In this paper, we present a tool-supported approach to quantitative graph-based security risk modeling and analysis based on attack-defense trees. Our approach is based on QFLan, a successful domain-specific approach to support quantitative modeling and analysis of highly configurable systems, whose domain-specific components have been decoupled to facilitate the instantiation of the QFLan approach in the domain of graph-based security risk modeling and analysis. Our approach incorporates distinctive features from three popular kinds of attack trees, namely enhanced attack trees, capabilities-based attack trees and attack countermeasure trees, into the domain-specific modeling language. The result is a new framework, called RisQFLan, to support quantitative security risk modeling and analysis based on attack-defense diagrams. By offering either exact or statistical verification of probabilistic attack scenarios, RisQFLan constitutes a significant novel contribution to the existing toolsets in that domain. We validate our approach by highlighting the additional features offered by RisQFLan in three illustrative case studies from seminal approaches to graph-based security risk modeling analysis based on attack trees.Source: ISTI Technical Report, ISTI-2021-TR/001, pp.1–16, 2021
DOI: 10.32079/isti-tr-2021/001
Project(s): CyberSec4Europe via OpenAIRE

See at: ISTI Repository Open Access | CNR ExploRA Open Access


2021 Conference article Open Access OPEN

A clean and efficient implementation of choreography synthesis for behavioural contracts
Basile D., Ter Beek M. H.
The Contract Automata Tool is an open-source tool for the specification, composition and synthesis of coordination of service contracts, including functionalities to deal with modalities and configurations. We discuss an implementation of the abstract parametric synthesis algorithm firstly introduced in our COORDINATION 2019 paper, comprehending most permissive controller, orchestration and choreography synthesis. The tool's source code has been redesigned and refactored in Java 8, and we show the resulting gain in computational efficiency.Source: COORDINATION 2021 - 23rd IFIP WG 6.1 International Conference on Coordination Models and Languages, pp. 225–238, Online conference, 14-18/06/2021
DOI: 10.1007/978-3-030-78142-2_14

See at: ISTI Repository Open Access | link.springer.com Restricted | CNR ExploRA Restricted


2021 Conference article Open Access OPEN

Supervisory synthesis of configurable behavioural contracts with modalities
Basile D., Ter Beek M. H., Degano P., Legay A., Ferrari G. L., Gnesi S., Di Giandomenico F.
Service contracts characterise the desired behavioural compliance of a composition of services, typically defined by the fulfilment of all service requests through service offers. Contract automata are a formalism for specifying behavioural service contracts. Based on the notion of synthesis of the most permissive controller from Supervisory Control Theory, a safe orchestration of contract automata can be computed that refines a composition into a compliant one. This short paper summarises the contributions published in [8], where we endow contract automata with two orthogonal layers of variability: (i) at the structural level, constraints over service requests and offers define different configurations of a contract automaton, depending on which requests and offers are selected or discarded; and (ii) at the behavioural level, service requests of different levels of criticality can be declared, which induces the novel notion of semi-controllability. The synthesis of orchestrations is thus extended to respect both the structural and the behavioural variability constraints. Finally, we show how to efficiently compute the orchestration of all configurations from only a subset of these configurations. A recently redesigned and refactored tool supports the developed theory.Source: FORTE 2021 - 41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, pp. 177–181, Online conference, 14-18/06/2021
DOI: 10.1007/978-3-030-78089-0_10

See at: ISTI Repository Open Access | link.springer.com Restricted | CNR ExploRA Restricted


2021 Journal article Open Access OPEN

Quantitative security risk modeling and analysis with RisQFLan
Ter Beek M. H., Legay A., Lluch Lafuente A., Vandin A.
Domain-specific quantitative modeling and analysis approaches are fundamental in scenarios in which qualitative approaches are inappropriate or unfeasible. In this paper, we present a tool-supported approach to quantitative graph-based security risk modeling and analysis based on attack-defense trees. Our approach is based on QFLan, a successful domain-specific approach to support quantitative modeling and analysis of highly configurable systems, whose domain-specific components have been decoupled to facilitate the instantiation of the QFLan approach in the domain of graph-based security risk modeling and analysis. Our approach incorporates distinctive features from three popular kinds of attack trees, namely enhanced attack trees, capabilities-based attack trees and attack countermeasure trees, into the domain-specific modeling language. The result is a new framework, called RisQFLan, to support quantitative security risk modeling and analysis based on attack-defense diagrams. By offering either exact or statistical verification of probabilistic attack scenarios, RisQFLan constitutes a significant novel contribution to the existing toolsets in that domain. We validate our approach by highlighting the additional features offered by RisQFLan in three illustrative case studies from seminal approaches to graph-based security risk modeling analysis based on attack trees.Source: Computers & security 109 (2021). doi:10.1016/j.cose.2021.102381
DOI: 10.1016/j.cose.2021.102381
Project(s): CyberSec4Europe via OpenAIRE

See at: ISTI Repository Open Access | CNR ExploRA Restricted | www.sciencedirect.com Restricted


2021 Contribution to journal Open Access OPEN

Formal methods: practical applications and foundations
Ter Beek M. H., Mciver A.
Source: Formal methods in system design 58 (2021): 1–4. doi:10.1007/s10703-021-00380-6
DOI: 10.1007/s10703-021-00380-6

See at: ISTI Repository Open Access | link.springer.com Restricted | CNR ExploRA Restricted


2021 Report Open Access OPEN

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. 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.Source: ISTI-TR-2021/006, 2021
DOI: 10.32079/isti-tr-2021/006
Project(s): 4SECURAIL via OpenAIRE, ASTRail via OpenAIRE

See at: ISTI Repository Open Access | CNR ExploRA Open Access


2021 Report Open Access OPEN

Systematic evaluation and usability analysis of formal tools for railway system design
Ferrari A., Mazzanti F., Basile D., Ter Beek M. H.
Formal methods and supporting tools have a long record of success in the development of safety-critical systems. However, no single tool has emerged as the dominant solution for system design. Each tool differs from the others in terms of the modeling language used, its verification capabilities and other complementary features, and each development context has peculiar needs that require different tools. This is particularly problematic for the railway industry, in which formal methods are highly recommended by the norms, but no actual guidance is provided for the selection of tools. To guide companies in the selection of the most appropriate formal tools to adopt in their contexts, a clear assessment of the features of the currently available tools is required. To address this goal, this paper considers a set of 13 formal tools that have been used for railway system design, and it presents a systematic evaluation of such tools and a preliminary usability analysis of a subset of 7 tools, involving railway practitioners. The results are discussed considering the most desired aspects by industry and earlier related studies. While the focus is on the railway domain, the overall methodology can be applied to similar contexts. Our study thus contributes with a systematic evaluation of formal tools and it shows that despite the poor graphical interfaces, usability and maturity of the tools are not major problems, as claimed by contributions from the literature. Instead, support for process integration is the most relevant obstacle for the adoption of most of the tools.Source: ISTI-2021-TR/007, 2021
DOI: 10.32079/isti-tr-2021/007
Project(s): 4SECURAIL via OpenAIRE, ASTRail via OpenAIRE

See at: CNR ExploRA Open Access


2021 Report Open Access OPEN

Featured team automata
Ter Beek M. H., Cledou G., Hennicker R., Proença J.
We propose featured team automata to support variability in the development and analysis of teams, which are systems of reactive components that communicate according to specified synchronisation types. A featured team automaton concisely describes a family of concrete product models for specific configurations determined by feature selection. We focus on the analysis of communication-safety properties, but doing so product-wise quickly becomes impractical. Therefore, we investigate how to lift notions of receptiveness (no message loss) to the level of family models. We show that featured (weak) receptiveness of featured team automata characterises (weak) receptiveness for all product instantiations. A prototypical tool supports the developed theory.Source: ISTI-TR-2021/008, pp.1–22, 2021
DOI: 10.32079/isti-tr-2021/008

See at: ISTI Repository Open Access | CNR ExploRA Open Access


2021 Conference article Open Access OPEN

Spatial Model Checking for Smart Stations: Research Challenges
Ter Beek M. H., Ciancia V., Latella D., Massink M., Spagnolo G. O.
In this position paper, we discuss the introduction of spatial verification techniques in an application scenario from smart stations, viz. analysing the user experience with respect to the lighting conditions of station areas. This is a case study in industrial projects. We discuss three challenging use cases for the application of spatial model checking in this setting. First, we envision how to use the spatial model checker VoxLogicA, which can analyse both 2D and 3D voxel-based maps, to explore the areas that users can visit in a station area and to characterise them with respect to their illumination conditions. This is aimed at monitoring a smart station. We also ideate statistical spatio-temporal model checking of the design of energy-saving protocols, exploiting the modelling of user preferences. Finally, we discuss the idea of quantifying the impact of design changes, based on the logs of smart stations, to identify and measure the incidence of undesired events (e.g. non-illuminated platforms where a train is passing by) before and after each change.Source: FMICS 2021 - 26th International Conference on Formal Methods for Industrial Critical Systems, pp. 39–47, Online conference, 24-26/08/2021
DOI: 10.1007/978-3-030-85248-1_3

See at: ISTI Repository Open Access | link.springer.com Restricted | CNR ExploRA Restricted


2021 Contribution to journal Open Access OPEN

Editorial
Mciver A., Ter Beek M. H.
Source: Formal aspects of computing 33 (2021): 459–460. doi:10.1007/s00165-021-00559-y
DOI: 10.1007/s00165-021-00559-y

See at: link.springer.com Open Access | ISTI Repository Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2021 Contribution to conference Open Access OPEN

25th International Systems and Software Product Line Conference. Proceedings - Volume A
Mousavi M., Schobbens P. Y., Araujo H., Schaefer I., Ter Beek M. H., Devroey X., Rojas J. M., Pinto M., Teixeira L., Berger T., Noppen J., Reinhartz-Berger I., Temple P., Damiani F., Petke J.
Welcome to SPLC 2021, the 25th International Systems and Software Product Line Conference. Variability is at the core of most modern computer and cyber-physical systems. Product lines provide a structured method for dealing with variability. They represent one of the most exciting paradigm shifts in software and systems development, with new challenges and opportunities for both research and practice. For decades, SPLC has been the ?agship venue for practitioners, researchers, and educators interested in systems and software product lines. SPLC is a great venue for learning about the state of the art as well as practice, trends, innovations, industry experiences, and challenges in the area of systems family engineering at large. SPLC 2021 took place from September 6th to 11th.Source: New York: ACM Press, 2021
DOI: 10.1145/3461001

See at: dl.acm.org Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2021 Contribution to conference Open Access OPEN

25th International Systems and Software Product Line Conference. Proceedings - Volume B
Mousavi M., Schobbens P. Y., Araujo H., Schaefer I., Ter Beek M. H., Devroey X., Rojas J. M., Rabiser R., Varshosaz M., Kishi T., Lee J.
Welcome to SPLC 2021, the 25th International Systems and Software Product Line Conference. Variability is at the core of most modern computer and cyber-physical systems. Product lines provide a structured method for dealing with variability. They represent one of the most exciting paradigm shifts in software and systems development, with new challenges and opportunities for both research and practice. For decades, SPLC has been the ?agship venue for practitioners, researchers, and educators interested in systems and software product lines. SPLC is a great venue for learning about the state of the art as well as practice, trends, innovations, industry experiences, and challenges in the area of systems family engineering at large. SPLC 2021 took place from September 6th to 11th.Source: New York: ACM Press, 2021
DOI: 10.1145/3461002

See at: dl.acm.org Open Access | CNR ExploRA Open Access


2021 Conference article Open Access OPEN

Static analysis and family-based model checking of featured transition systems with VMC
Ter Beek M. H., Mazzanti F., Damiani F., Paolini L., Scarso G., Valfrè M., Lienhardt M.
A Featured Transition System (FTS) is a formalism for modeling variability in configurable system behavior. The behavior of all variants (products) is modeled in a single compact FTS by associating the possibility to perform an action and transition from one state to another with feature expressions that condition the execution of an action in specific variants. We present a front-end for the research tool VMC. The resulting toolchain allows a modeler to analyze an FTS for ambiguities (dead or false optional transitions and hidden deadlock states), transform an ambiguous FTS into an unambiguous one, and perform an efficient kind of family-based verification of an FTS without hidden deadlock states. We use benchmarks from the literature to demonstrate the novelties offered by the toolchain.Source: SPLC'21 - 25th ACM International Systems and Software Product Line Conference, pp. 24–27, Leicester, UK, 06-10/09/2021
DOI: 10.1145/3461002.3473071

See at: ISTI Repository Open Access | dl.acm.org Restricted | CNR ExploRA Restricted