237 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
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 (2021). 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


2021 Conference article Open Access OPEN

Static analysis and family-based model checking with VMC
Ter Beek M. H., Mazzanti F., Damiani F., Paolini L., Scarso G., Lienhardt M.
VMC is a research tool for model checking variability-rich behavioural models specified as a modal transition system (MTS) with variability constraints (MTSv). In this tutorial, we introduce a tool chain built on VMC that allows to perform an efficient kind of family-based model checking in absence of deadlocks. It accepts as input either an MTSv or a featured transition system (FTS).Source: SPLC'21 - 25th International Systems and Software Product Line Conference, pp. 214–214, Leicester, UK, 06-10/09/2021
DOI: 10.1145/3461001.3472732

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


2020 Conference article Open Access OPEN

Variability meets security: quantitative security modeling and analysis of highly customizable attack scenarios
Ter Beek M. H. Legay A., Lluch Lafuente A., Vandin A.
We present a framework for quantitative security modeling and analysis of highly customizable attack scenarios, which resulted as a spin-off from our research in software product line engineering. The graphical security models are based on attributed attack-defense diagrams to capture the structure and properties of vulnerabilities, defenses and countermeasures--with notable similarities to feature diagrams--and on probabilistic models of attack behavior, capable of capturing resource constraints and attack effectiveness. In this paper, we provide an overview of the framework that is described in full technical detail in twin papers, which present the formal syntax and semantics of the domain-specific language and showcase the associated tool with advanced IDE support for performing analyses based on statistical model checking. The properties of interest range from average cost and success probability of attacks to the effectiveness of defenses and countermeasures. Here we illustrate the capabilities of the DSL and the tool by applying them to an example scenario from the security domain. This shows how techniques from variability modeling can be applied to security. We conclude with a vision and roadmap for future research.Source: VaMoS'20 - 14th International Working Conference on Variability Modelling of Software-Intensive Systems, pp. 11:1–11:9, Magdeburg, Germany, 5-7 February 2020
DOI: 10.1145/3377024.3377041
Project(s): CyberSec4Europe via OpenAIRE

See at: backend.orbit.dtu.dk Open Access | ISTI Repository Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | dl.acm.org Restricted | dl.acm.org Restricted | CNR ExploRA Restricted


2020 Conference article Open Access OPEN

Family-based SPL model checking using parity games with variability
Ter Beek M. H., Van Loo S., De Vink E. P., Willemse T. A. C.
Family-based SPL model checking concerns the simultaneous verification of multiple product models, aiming to improve on enumerative product-based verification, by capitalising on the common features and behaviour of products in a software product line (SPL), typically modelled as a featured transition system (FTS). We propose efficient family-based SPL model checking of modal mu-calculus formulae on FTSs based on variability parity games, which extend parity games with conditional edges labelled with feature configurations, by reducing the SPL model checking problem for the modal mu-calculus on FTSs to the variability parity game solving problem, based on an encoding of FTSs as variability parity games. We validate our contribution by experiments on SPL benchmark models, which demonstrate that a novel family-based algorithm to collectively solve variability parity games, using symbolic representations of the configuration sets, outperforms the product-based method of solving the standard parity games obtained by projection with classical algorithms.Source: FASE 2020 - International Conference on Fundamental Approaches to Software Engineering, pp. 245–265, Dublin, Ireland, 25-30/04/2020
DOI: 10.1007/978-3-030-45234-6_12

See at: Europe PubMed Central Open Access | link.springer.com Open Access | link.springer.com Open Access | ISTI Repository Open Access | CNR ExploRA Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | link.springer.com Restricted | link.springer.com Restricted | rd.springer.com Restricted


2020 Journal article Open Access OPEN

Synthesis of orchestrations and choreographies: bridging the gap between supervisory control and coordination of services
Basile D., Ter Beek M. H., Pugliese R.
We present a number of contributions to bridging the gap between supervisory control theory and coordination of services in order to explore the frontiers between coordination and control systems. Firstly, we modify the classical synthesis algorithm from supervisory control theory for obtaining the so-called most permissive controller in order to synthesise orchestrations and choreographies of service contracts formalised as contract automata. The key ingredient to make this possible is a novel notion of controllability. Then, we present an abstract parametric synthesis algorithm and show that it generalises the classical synthesis as well as the orchestration and choreography syntheses. Finally, through the novel abstract synthesis, we show that the concrete syntheses are in a refinement order. A running example from the service domain illustrates our contributions.Source: Logical Methods in Computer Science 16 (2020). doi:10.23638/LMCS-16(2:9)2020
DOI: 10.23638/lmcs-16(2:9)2020

See at: arXiv.org e-Print Archive Open Access | lmcs.episciences.org Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2020 Conference article Open Access OPEN

Team Automata@Work: On Safe Communication
Ter Beek M. H., Hennicker R., Kleijn J.
We study requirements for safe communication in systems of reactive components in which components communicate via synchronized execution of common actions. These systems are modelled in the framework of team automata in which any number of components can participate--as a sender or as a receiver--in the execution of a communication action. Moreover, there is no fixed synchronisation policy as these policies in general depend on the application. In this short paper, we reconsider the concept of safe communication in terms of reception and responsiveness requirements, originally defined for synchronisation policies determined by a synchronisation type. Illustrated by a motivating example, we propose three extensions. First, compliance, i.e. satisfaction of communication requirements, does not have to be immediate. Second, the synchronisation type (and hence the communication requirements) no longer has to be uniform, but can be specified per action. Third, we introduce final states to be able to distinguish between possible and guaranteed executions of actions.Source: 22nd IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION'20), pp. 77–85, Valletta, Malta, 15-19 June 2020
DOI: 10.1007/978-3-030-50029-0_5

See at: Europe PubMed Central Open Access | link.springer.com Open Access | ISTI Repository Open Access | academic.microsoft.com Restricted | Mémoires en Sciences de l'Information et de la Communication Restricted | Mémoires en Sciences de l'Information et de la Communication Restricted | Mémoires en Sciences de l'Information et de la Communication Restricted | link.springer.com Restricted | link.springer.com Restricted | link.springer.com Restricted | CNR ExploRA Restricted | rd.springer.com Restricted | www.scilit.net Restricted


2020 Conference article Open Access OPEN

Strategy Synthesis for Autonomous Driving in a Moving Block Railway System with Uppaal Stratego
Basile D., Ter Beek M. H., Legay A.
Moving block railway systems are the next generation signalling systems currently under development as part of the Shift2Rail European initiative, including autonomous driving technologies. In this paper, we model a suitable abstraction of a moving block signalling system with autonomous driving as a stochastic priced timed game. We then synthesise safe and optimal driving strategies for the model by applying advanced techniques that combine statistical model checking with reinforcement learning as provided by Uppaal Stratego. Hence, we show the applicability of Uppaal Stratego in this concrete case study.Source: 40th IFIP WG 6.1 International Conference on FORmal TEchniques for Distributed Objects, Components, and Systems (FORTE'20), pp. 3–21, Valletta, Malta, 15-19/06/2020
DOI: 10.1007/978-3-030-50086-3_1
Project(s): 4SECURAIL via OpenAIRE

See at: Europe PubMed Central Open Access | link.springer.com Open Access | ISTI Repository Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | dial.uclouvain.be Restricted | Mémoires en Sciences de l'Information et de la Communication Restricted | Mémoires en Sciences de l'Information et de la Communication Restricted | Mémoires en Sciences de l'Information et de la Communication Restricted | link.springer.com Restricted | link.springer.com Restricted | CNR ExploRA Restricted | rd.springer.com Restricted


2020 Conference article Open Access OPEN

Comparing formal tools for system design: a judgment study
Ferrari A, Mazzantif., Basile D., Ter Beek M. H., Fantechi A.
Formal methods and tools have a long history of successful applications in the design of safety-critical railway products. However, most of the experiences focused on the application of a single method at once, and little work has been performed to compare the applicability of the different available frameworks to the railway context. As a result, companies willing to introduce formal methods in their development process have little guidance on the selection of tools that couldfi t their needs. To address this goal, this paper presents a comparison between 9 different formal tools, namely Atelier B, CADP, FDR4, NuSMV, ProB, Simulink, SPIN, UMC, and UPPAAL SMC. We performed a judgment study, involving 17 experts with experience in formal methods applied to railways. In the study, part of the experts were required to model a railway signaling problem (a moving-block train distancing system) with the different tools, and to provide feedback on their experience. The information produced was then synthesized, and the results were validated by the remaining experts. Based on the outcome of this process, we provide a synthesis that describes when to use a certain tool, and what are the problems that may be faced by modelers. Our experience shows that the different tools serve different purposes, and multiple formal methods are required to fully cover the needs of the railway system design process.Source: ICSE'20 - 42nd International Conference on Software Engineering, pp. 62–74, Seoul, Republic of Korea, 27/6/2020-19/7/2020
DOI: 10.1145/3377811.3380373
Project(s): 4SECURAIL via OpenAIRE, ASTRail via OpenAIRE

See at: ISTI Repository Open Access | 2020.icse-conferences.org Restricted | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | dl.acm.org Restricted | ieeexplore.ieee.org Restricted | CNR ExploRA Restricted