130 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 Conference article Open Access OPEN

Formal modeling and initial analysis of the 4SECURail case study
Mazzanti F., Belli D.
We present the case study developed in the context of the 4SECURail project and the approach used for its formal modeling and analysis. Starting from a simple SysML/UML behavioral model of the system requirements, three formal models have been developed using three different frameworks, namely UMC, ProB, and CADP/LNT. The paper shows how the different ways to represent and analyze the system from the three different points of view allow us to take advantage of the resulting diversity.Source: MARS 2022 - Fifth Workshop on Models for Formal Analysis of Real Systems, pp. 118–144, Munich, DE, 01/04/2022
DOI: 10.4204/eptcs.355.6
Project(s): 4SECURAIL via OpenAIRE

See at: eptcs.web.cse.unsw.edu.au Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2021 Journal article Open Access OPEN

Compositional Verification of Concurrent Systems by Combining Bisimulations
Frédéric Lang F. Mateescu R., Mazzanti F.
One approach to verify a property expressed as a modal ?-calculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes in a hierarchical way, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the Ldbr fragment? of the ?-calculus (consisting of weak modalities only), individual processes can be minimized modulo divergence-preserving branching (divbranching for short) bisimulation. In this paper, we refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or div-branching bisimulation minimization on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend Ldbr with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems. In particular, we applied our approach to the verification problems of the RERS 2019 challenge and observed drastic reductions of the state space compared to the approach in which only strong bisimulation minimization is used, on formulas not preserved by divbranching bisimulation.Source: Formal methods in system design (Dordr., Online) (2021). doi:10.1007/s10703-021-00360-w
DOI: 10.1007/s10703-021-00360-w
DOI: 10.1007/978-3-030-30942-8_13
Project(s): 4SECURAIL via OpenAIRE

See at: hal.inria.fr Open Access | ISTI Repository Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | Hyper Article en Ligne Restricted | Hyper Article en Ligne Restricted | hal.inria.fr Restricted | Hyper Article en Ligne Restricted | Hal-Diderot Restricted | Hal-Diderot Restricted | Hal-Diderot Restricted | link.springer.com Restricted | Formal Methods in System Design Restricted | link.springer.com Restricted | link.springer.com Restricted | Formal Methods in System Design Restricted | CNR ExploRA Restricted


2021 Report Open Access OPEN

4SECURail - Technical Informative Note 15 - Progress Report: Formal development Demonstrator Prototype
Mazzanti F., Belli D.
This Technical Informative Note describes the progress of the activity of Work Package 2 / Task 2.3 in the months 12-17 of the project 4SECURail. The final results of Task 2.3 will be described in Deliverable 2.5, due at month 20 (end of July 2021). This Technical Informative Note is likely to already contain most of the interesting results that will appear in the final deliverable, together with other less important internal progress details that for readability issues will not appear in the final version. The overall final purpose of the whole experimentation is the observation of the impact, in our specific case, i.e. applying our specific tools and methodologies1 to our specific case study2, of the adoption of formal methods towards the improvement of the quality of the system specifications under construction.Source: Project report, 4SECURail, TIN-FM-15, pp.1–53, 2021
Project(s): 4SECURAIL 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 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


2021 Report Open Access OPEN

4SECURail - Revised requirements of the 4SECURail case study
Mazzanti F., Belli D.
The final version of the system requirements of the case study used in the 4SECURail demonstratorSource: ISTI Project report, 4SECURail, 2021
DOI: 10.5281/zenodo.5541217
Project(s): 4SECURAIL via OpenAIRE

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


2021 Software Unknown

Formal models of the SAI/CSL system of the 4SECURail case study
Mazzanti F., Belli D.
Formal models of 4SECURAIL case study in the notation accepted by UMC, ProB, CADP/LNTDOI: 10.5281/zenodo.5541307
Project(s): 4SECURAIL via OpenAIRE

See at: CNR ExploRA


2021 Software Unknown

The UMC2LNT and UMC2PROB model transformation tools
Mazzanti F., Belli D.
This documents contains the source code of two trasformation tools used in the 4SECURail project. The tools umc2lnt takes as argument the name of a file contining an UMC model and generates the corresponding CADP/LNT model.DOI: 10.5281/zenodo.5541350
Project(s): 4SECURAIL via OpenAIRE

See at: CNR ExploRA


2021 Report Open Access OPEN

4SECURail - Formal development demonstrator prototype, final release
Mazzanti F., Belli D.
This Deliverable describes the final results of Task 2.3 of 4SECURail project. The goal of Task 2.3 is to apply the formal development demonstrator process defined in Task 2.1 to the signalling case study defined in Task 2.2 and to describe the observed impact of the selected tools and methodologies for improving the quality of the system specifications under analysis.Source: ISTI Project report, 4SECURail, 2021
Project(s): 4SECURAIL via OpenAIRE

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


2021 Journal article Open Access OPEN

Systematic evaluation and usability analysis of formal methods tools for railway signaling 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 methods 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 methods tools that have been used for the early design of railway systems, 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 signaling domain, the overall methodology can be applied to similar contexts. Our study thus contributes with a systematic evaluation of formal methods 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. Our contribution can be useful to R&D engineers from railway signaling companies and infrastructure managers, but also to tool developers and academic researchers alike.Source: IEEE transactions on software engineering (2021). doi:10.1109/TSE.2021.3124677
DOI: 10.1109/tse.2021.3124677
Project(s): 4SECURAIL via OpenAIRE, ASTRail via OpenAIRE

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


2020 Conference article Open Access OPEN

Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities
Lang F., Mateescu R., Mazzanti F.
We showed in a recent paper that, when verifying a modal?-calculus formula, the actions of the system under verification can bepartitioned into sets of so-called weak and strong actions, depending onthe combination of weak and strong modalities occurring in the formula.In a compositional verification setting, where the system consists of pro-cesses executing in parallel, this partition allows us to decide whethereach individual process can be minimized for either divergence-preservingbranching (if the process contains only weak actions) or strong (other-wise) bisimilarity, while preserving the truth value of the formula. In thispaper, we refine this idea by devising a family of bisimilarity relations,named sharp bisimilarities, parameterized by the set of strong actions.We show that these relations have all the nice properties necessary tobe used for compositional verification, in particular congruence and ad-equacy with the logic. We also illustrate their practical utility on severalexamples and case-studies, and report about our success in the RERS2019 model checking challenge.Source: 26th International Conference, TACAS 2020, pp. 57–73, Dublin, Ireland, April 25-30, 2020
DOI: 10.1007/978-3-030-45237-7_4

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 | INRIA a CCSD electronic archive server Restricted | INRIA a CCSD electronic archive server Restricted | INRIA a CCSD electronic archive server Restricted | link.springer.com Restricted | link.springer.com Restricted


2020 Journal article Open Access OPEN

A Formal Methods Demonstrator for Railways
Mazzanti F., Basile D.
The 4SECURail project - funded by the European UnionHorizon 2020 Shift2Rail Joint Undertaking - has twooverall objectives: to design a Computer Security IncidentResponse Team (CSIRT) for joint EU-Rail cybersecurity,and the setup of a Formal Methods Demonstrator for theevaluation, in terms of cost, benefits and requiredlearning curve, of the impact of the use of FormalMethods for the rigorous specification of thecomponents of a railway signalling infrastructure.Source: ERCIM news online edition 121 (2020).

See at: ercim-news.ercim.eu Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


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


2020 Conference article Open Access OPEN

Designing a demonstrator of formal methods for railways infrastructure managers
Basile D., Ter Beek M. H., Fantechi A., Ferrari A., Gnesi S., Masullo L., Mazzanti F., Piattino A., Trentini D.
The Shift2Rail Innovation Programme (IP) is focussing on innovative technologies to enhance the overall railway market segments. Formal methods and standard interfaces have been identified as two key concepts to reduce time-to-market and costs, while ensuring safety, interoperability and standardisation. However, the decision to start using formal methods is still deemed too risky. Demonstrating technical and commercial benefits of both formal methods and standard interfaces is necessary to address the obstacles of learning curve and lack of clear cost/benefit analysis that are hindering their adoption, and this is the goal of the 4SECURail project, recently funded by the Shift2Rail IP. In this paper, we provide the reasoning and the rationale for designing the formal methods demonstrator for the 4SECURail project. The design concerns two important issues that have been analysed: (i) the usefulness of formal methods from the point of view of the infrastructure managers, (ii) the adoption of a semi-formal SysML notation within our formal methods demonstrator process.Source: ISoLA'20 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Applications, pp. 467–485, Rhodes, Greece, 20-30 October, 2020
DOI: 10.1007/978-3-030-61467-6_30
Project(s): 4SECURAIL via OpenAIRE

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


2020 Report Open Access OPEN

4SECURail - D.2.1: Specification of formal development demonstrator
Mazzanti F., Basile D., Fantechi A., Gnesi S., Ferrari A., Piattino A., Masullo L., Trentini D.
The overall goal of the Workstream 1 "Demonstrator Development for the use of Formal Methods in Railway Environment", spreading on the activities of Tasks 2.1, 2.2, 2.3 2.4 of the 4SecuRail project is: - the definition of a "formal methods demonstrator process" (shortly Demonstrator) for the rigorous construction and analysis of system specifications (from the point of view of infrastructure managers); - the application of the Demonstrator process to a railway signalling system case study; - with the goal of performing a cost benefits analysis and the evaluation of the required learning curve for the application of this Demonstrator process This Deliverable "Specification of formal development demonstrator", describing the result of the first part of Task 2.1, presents the overall structure of the Demonstrator process and illustrates the selected choices for its architecture, both in terms of methodologies and tools. The specified formal development demonstrator will be experimented with its application to a simple initial case study in the second part of Task 2.1. The experience gained with this initial experimentation will result in the consolidation of the definition of the Demonstrator process prototype (reported in the Deliverable D2.2 of Task 2.1 "Formal development demonstrator prototype - 1st release"). The consolidated process will then be applied in Task 2.3 to the complete case study defined in Task 2.2 and that activity will provide the reference for the costs-benefits analysis of Task 2.4.Source: Project Report, 4SECURail, D2.1, 2020
Project(s): 4SECURAIL via OpenAIRE

See at: ISTI Repository Open Access | CNR ExploRA Open Access | www.4securail.eu Open Access


2020 Report Open Access OPEN

4SECURail - D.2.2 : Formal development Demonstrator prototype - 1st release
Mazzanti F., Basile D.
This deliverable: "Formal development Demonstrator prototype, 1st Release", completes the description of the selected Demonstrator process (identifying the chosen MBSD framework for UML-based modelling and simulation) and describes how the defined Demonstrator process has been exercised in Task 2.1 with an initial fragment of the case study identified in Task 2.2. The initial fragment concerns the modelling and analysis of a Communication Supervision Layer (CSL), specifically dedicated to the control of the communication status between two neighbouring Radio Block Centre (RBC), over the Safe Application Intermediate sub-Layer (SAI) sublevel of the architecture.Source: Project Report, 4SECURail, D2.2, pp.1–85, 2020
Project(s): 4SECURAIL via OpenAIRE

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


2019 Journal article Open Access OPEN

On the expressiveness of modal transition systems with variability constraints
Ter Beek M., Damiani F., Gnesi S., Mazzanti F., Paolini L.
We demonstrate that modal transition systems with variability constraints are equally expressive as featured transition systems, by defining a transformation of the latter into the former, a transformation of the former into the latter, and proving the soundness and completeness of both transformations. Modal transition systems and featured transition systems are widely recognised as fundamental behavioural models for software product lines and our results thus contribute to the expressiveness hierarchy of such basic models studied in other papers published in this journal.Source: Science of computer programming (Print) 169 (2019): 1–17. doi:10.1016/j.scico.2018.09.006
DOI: 10.1016/j.scico.2018.09.006

See at: ISTI Repository Open Access | Science of Computer Programming Restricted | Science of Computer Programming Restricted | Science of Computer Programming Restricted | Science of Computer Programming Restricted | CNR ExploRA Restricted | Science of Computer Programming Restricted


2019 Conference article Open Access OPEN

Survey on formal methods and tools in railways: the ASTRail approach
Ferrari A., Ter Beek M. H., Mazzanti F., Basile D., Fantechi A., Gnesi S., Piattino A., Trentini D.
Formal methods and tools have been widely applied to the development of railway systems during the last decades. However, no universally accepted formal framework has emerged, and railway companies wishing to introduce formal methods have little guidance for the selection of the most appropriate methods and tools to adopt. A work package (WP) of the European project ASTRail, funded under the Shift2Rail initiative, addresses this problem, by performing a survey that considers scientific literature, international projects, and practitioners' perspectives to identify a collection of formal methods and tools to be applied in railways. This paper summarises the current results of this WP. We surveyed 114 scientific publications, 44 practitioners, and 8 projects to come to a shortlist of 14 methods considered suitable for system modelling and verification in railways. The methods and tools were reviewed according to a set of functional, language-related, and quality features. The current paper extends the body of knowledge with a set of publicly available documents that can be leveraged by companies for guidance on formal methods selection in railway system development.Source: RSSRail'19 - Third International Conference on Reliability, Safety, and Security of Railway Systems, pp. 226–241, Lille, France, 04-06 June 2019
DOI: 10.1007/978-3-030-18744-6_15
Project(s): ASTRail via OpenAIRE

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