123 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 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


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


2019 Contribution to book Open Access OPEN

States and Events in KandISTI: A Retrospective
Ter Beek M. H., Fantechi A., Gnesi S., Mazzanti F.
Early work on automated formal verification produced pioneering model-checking algorithms, in which system computations were modelled either as sequences of distinguished states in which the system evolves or as sequences of events or actions occurring during the system's state transitions. In both cases, automata-like structures generally known as transition systems were exploited to capture all possible computations, but still either state-based or event-based. Many years later, both views were combined in descriptions of computations as the evolution between distinguished states by means of transitions characterised by the occurrence of events, and verification tools were adapted to this more general setting. Meanwhile, the most important drive in improving verification tools concerned the complexity of models, which was attacked by algorithms capable of minimising the information needed for deciding the verification questions. One of the outcomes of this quest was local, on-the-fly model checking. Both of these lines of research, pioneered by Bernhard Steffen, are discussed in this paper in a general retrospective on state-based and event-based models of transition systems and temporal logics, followed by an overview of how this is exploited in the KandISTI model-checking environment.Source: Models, Mindsets, Meta: The What, the How, and the Why Not?, edited by Margaria T.; Graf S.; Larsen K.G., pp. 110–128. Berlin: Springer, 2019
DOI: 10.1007/978-3-030-22348-9_8

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


2019 Conference article Open Access OPEN

Static Analysis of Featured Transition Systems
Ter Beek M. H., Damiani F., Lienhardt M., F. Mazzanti F., Paolini L.
A Featured Transition System (FTS) is a formal behavioural model for software product lines, which represents the behaviour of all the products of an SPL in a single compact structure by associating transitions with features that condition their existence in products. In general, an FTS may contain featured transitions that are unreachable in any product (so called dead transitions) or, on the contrary, mandatorily present in all products for which their source state is reachable (so called false optional transitions), as well as states from which only for certain products progress is possible (so called hidden deadlocks). In this paper, we provide algorithms to analyse an FTS for such ambiguities and to transform an ambiguous FTS into an unambiguous FTS. The scope of our approach is twofold. First and foremost, an ambiguous model is typically undesired as it gives an unclear idea of the SPL. Second, an unambiguous FTS paves the way for efficient family-based model checking. We apply our approach to illustrative examples from the literature.Source: 23rd International Systems and Software Product Line Conference (SPLC'19), pp. 39–51, Paris, France, 9-13 September 2019
DOI: 10.1145/3336294.3336295

See at: hal.archives-ouvertes.fr Open Access | Archivio Istituzionale Open Access | ISTI Repository Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | dl.acm.org Restricted | dl.acm.org 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 | CNR ExploRA Restricted


2019 Conference article Open Access OPEN

Adopting Formal Methods in an Industrial Setting: The Railways Case
Ter Beek M. H., Boraelv A., Fantechi A., Ferrari A., Gnesi S., Loefving C., Mazzanti F.
The railway sector has seen a large number of successful applications of formal methods and tools. However, up-to-date, structured information about the industrial usage and needs related to formal tools in railways is limited. Two Shift2Rail projects, X2Rail-2 and ASTRail, have addressed this issue by performing a systematic search over the state of the art of formal methods application in railways to identify the best used practices. As part of the work of these projects, questionnaires on formal methods and tools have been designed to gather input and guidance on the adoption of formal methods in the railway domain. Even though the questionnaires were developed independently and distributed to different audiences, the responses show a certain convergence in the replies to the questions common to both. In this paper, we present a detailed report on such convergence, drawing some indications about methods and tools that are considered to constitute the most fruitful approaches to industrial adoption.Source: FM 2019 - Third International Symposium on Formal Methods, pp. 762–772, Porto, Portugal, 7-11 October
DOI: 10.1007/978-3-030-30942-8_46
Project(s): ASTRail via OpenAIRE

See at: ISTI Repository Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | flore.unifi.it Restricted | link.springer.com Restricted | link.springer.com Restricted | link.springer.com Restricted | CNR ExploRA Restricted


2019 Conference article Open Access OPEN

A summary of: on the expressiveness of modal transition systems with variability constraints
Ter Beek M. H., Damiani F., Gnesi S, Mazzanti F., Paolini L.
Modal transition systems (MTSs) and featured transition systems (FTSs) are widely recognised as fundamental behavioural models for software product lines. This short paper summarises the contributions published in [3]: MTSs with variability constraints (MTS?s) are equally expressive as FTSs. This is proved by giving sound and complete transformations of the latter into the former, and of the former into the latter. The benefits of this result are twofold. First, it contributes to the expressiveness hierarchy of such basic models studied in the literature. Second, it provides an automatic algorithm from FTSs to MTS?s that preserves the original (compact) branching structure, thus paving the way for model checking FTSs with the variability model checker VMC.Source: IFM'19 - 15th International Conference on Integrated Formal Methods, pp. 542–546, Bergen, Norway, 2-6 December 2019
DOI: 10.1007/978-3-030-34968-4_34

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


2019 Contribution to book Restricted

A systematic approach to programming and verifying attribute-based communication systems
De Nicola R., Duong T., Inverso O., Mazzanti F.
A methodology is presented for the systematic development of systems of many components, that interact by relying on predicates over attributes that they themselves mutually expose. The starting point is a novel process calculus AbC (for Attribute-based Communication) introduced for modelling collective-adaptive systems. It is shown how to refine the model by introducing a translator from AbC into UML- like state machines that can be analyzed by UMC. In order to execute the specification, another translator is introduced that maps AbC terms into ABEL, a domain-specific framework that offers faithful AbC-style programming constructs built on top of Erlang. It is also shown how the proposed methodology can be used to assess relevant properties of systems and to automatically obtain an executable program for a non- trivial case study.Source: From Software Engineering to Formal Methods and Tools, and Back. Essays Dedicated to Stefania Gnesi on the Occasion of Her 65th Birthday, edited by Maurice H. ter Beek, Alessandro Fantechi, Laura Semini, pp. 377–396. Basel: Springer Nature Switzerland, 2019
DOI: 10.1007/978-3-030-30985-5_22

See at: academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | link.springer.com Restricted | link.springer.com Restricted | CNR ExploRA Restricted | www.scilit.net Restricted


2019 Conference article Open Access OPEN

Compositional verification of concurrent systems by combining bisimulations
Lang F., Mateescu R., Mazzanti F.
Compositional verification is a promising technique for analyzing action-based temporal properties of concurrent systems. 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, 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 Ldsbr fragment of ?-calculus (consistingofweakmodalitiesonly),individual processes can be minimized modulo divergence-sensitive branching (divbranching) 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 divbranching bisimulation minimiza- tion on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend the existing Ldsbr fragment 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.Source: FM 2019 -International Symposium on Formal Methods. Third World Congress, pp. 196–213, Porto, Portugal, 7-11 October 2019
DOI: 10.1007/978-3-030-30942-8_13
DOI: 10.1007/s10703-021-00360-w
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 | Formal Methods in System Design Restricted | link.springer.com Restricted | link.springer.com Restricted | Formal Methods in System Design Restricted | CNR ExploRA Restricted


2019 Report Open Access OPEN

ASTrail - Deliverable D4.3 - Validation Report
Ferrari A., Mazzanti F., Basile D., Fantechi A., Gnesi S., Trentini D., Piattino A., Sturani B.
Formal methods are mathematically-based techniques to support the development of software intensive systems. Normally, formal methods oriented to design and verification of systems include (i) a modelling language, which is used to model a system, and (ii) a verification strategy, which is used to verify properties on the system. Formal methods are usually associated to formal tools, which can provide textual or visual editors to create a model of the system, as well as automated verification capabilities. Formal methods have been largely applied in industrial projects, especially in the safety-critical market, including railways. However, it cannot yet be said that a single mature technology has emerged. The Work Package 4 (WP4) of the ASTRail project aims to identify, based on an analysis of the state-of-the- art and on concrete trials, the candidate set of formal and semi-formal methods that appear as the most adequate to be used in the railway context. In the following, when we will use the general term "formal method", we will implicitly include also semi-formal methods, i.e. those methods that use languages for which the semantics is not formally defined but depends on their execution engine. Since formal methods are normally associated with tools, we will also use the terms formal methods and formal tools interchangeably. To address the goal of identifying the most adequate formal methods, WP4 is structured into four tasks (T4.4, in bold, is the focus on the current deliverable): ? Task 4.1 - Benchmarking: this task aims at studying the state-of-the-art and state of the practice of formal and semi-formal methods, by gathering knowledge from the literature and railway practitioners. ? Task 4.2 - Ranking: this task aims at providing a ranking matrix to support the selection of the most adequate formal methods to be used in a certain development context. ? Task 4.3 - Trial Application: this task aims at experimenting the usage of a set of selected formal methods through the modelling of the moving-block system, from Task 2.1. ? Task 4.4 - Validation: this task aims at validating the usage of the selected formal methods by integrating the moving-block model with the automated driving technologies from Task 3.3. The current deliverable D4.3 Validation Report is the output of Task 4.4 - Validation. The results of Task 4.1- 2 and 4.3 have been reported in D4.1 and D4.2 respectively.Source: Project report, ASTRail, Deliverable D4.3, 2019
Project(s): ASTRail via OpenAIRE

See at: CNR ExploRA Open Access | www.astrail.eu Open Access