64 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
Rights operator: and / or
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 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 Journal article Open Access OPEN

Analysing an autonomous tramway positioning system with the Uppaal Statistical Model Checker
Basile D., Fantechi A., Rucher L., Mandò G.
The substitution of traditional occupancy detecting sensors with anAutonomous Positioning System (APS) is a promising solution tocontain costs and improve performance of current tramway signallingsystems. APS is an onboard system using satellite positioning andother inertial platforms to autonomously estimate the position ofthe tram with the needed levels of uncertainty and protection.However, autonomous positioning introduces, even in absence offaults, a quantitative uncertainty with respect to traditionalsensors. This paper investigates this issue in the context of anindustrial project: a model of the envisaged solution is proposed,and it is analysed using Uppaal Statistical Model Checker.A novel model-driven hazard analysis approach to the exploration ofemerging hazards is proposed. The analysis emphasises how thevirtualisation of legacy track circuits and on-board satellitepositioning equipment may give rise to new hazards, not present inthe traditional system.Source: Formal aspects of computing (2021). doi:10.1007/s00165-021-00556-1
DOI: 10.1007/s00165-021-00556-1

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


2021 Journal article Open Access OPEN

Secure multi-party computation with service contract automata
Basile D.
By combining research from model-based software engineering, dependable computing, and formal methods, it is possible to create a contract-based design methodology to enforce security accountability and reputation of distributed digital entities provided by potentially mutually distrusted organisations.Source: ERCIM news online edition 2021 (2021): 32–33.
Project(s): 4SECURAIL via OpenAIRE

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


2021 Conference article Open Access OPEN

Formal analysis of the UNISIG safety application intermediate sub-layer. Applying Formal Methods to railway standard interfaces
Basile D., Fantechi A., Rosadi I.
The combined use of standard interfaces and formal methods is currently under investigation by Shift2Rail, a joint undertaking between railway stakeholders and the EU. Standard interfaces are useful to increase market competition and standardization whilst reducing long-term life cycle costs. Formal methods are needed to achieve interoperability and safety of standard interfaces and are one of the targets of the 4SECURail project funded by Shift2Rail. This paper presents the modelling and analysis of the selected case study of the 4SECURail project: the Safe Application Intermediate sub-layer of the UNISIG RBC/RBC Safe Communication Interface. The adopted formal method is Statistical Model Checking of a network of Stochastic Priced Timed Automata, as provided by the Uppaal SMC tool. The main contributions are: (i) rigorous complete and publicly available models of an official interface specification already in operation, (ii) identification of safety and interoperability issues in the original specification using Statistical Model Checking, (iii) quantification of costs for learning the adopted formal method and developing the carried out analysis.Source: FMICS 2021 - 26th International Conference on Formal Methods for Industrial Critical Systems, pp. 174–190, Online conference, 24-26/08/2021
DOI: 10.1007/978-3-030-85248-1_11
Project(s): 4SECURAIL via OpenAIRE

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


2021 Master thesis Open Access OPEN

Analysing a safe communication protocol in the railway signaling domain with Timed Automata and Statistical Model Checking
Rosadi I.
This thesis focuses on the modeling and the safety requirements verification of a communication system in the railway signaling domain, where the use of standard interfaces and formal methods is increasing and is also expanding at the industrial level.Project(s): 4SECURAIL via OpenAIRE

See at: ISTI Repository Open Access | CNR ExploRA Restricted | sol.unifi.it Restricted


2021 Software Unknown

Contract automata library
Basile D.
The Contract Automata Tool is an ongoing basic research activity about implementing and experimenting with new developments in the theoretical framework of contract automata.

See at: github.com | CNR ExploRA


2021 Software Unknown

Contract automata application
Basile D.
This is a GUI application of the Contract Automata Toolkit, exploiting the contract automata library to put contract automata at work

See at: github.com | CNR ExploRA


2021 Software Unknown

Uppaal models and experiments for the paper: "Formal Analysis of the UNISIG Safety Application Intermediate Sublayer." (FMICS2021)
Basile D., Rosadi I.
Uppaal models of the paper Formal Analysis of the UNISIG Safety Application Intermediate Sublayer. FMICS2021 Basile, D., Fantechi, A. and Rosadi, I., 2021, August. Formal Analysis of the UNISIG Safety Application Intermediate Sub-layer. In International Conference on Formal Methods for Industrial Critical Systems (pp. 174-190). Springer, Cham. Video presentation: https://youtu.be/nGHfXi1vvg4 Mapping between the formulas described in the paper and the models ?4, ?5, ?7, ?9, ?11, ?13, ?17, ?18, ?19, ?20 -> modelConfStandard ?1, ?2, ?3, ?6, ?8, ?10, ?12, ?16 -> modelFastVerification ?14 -> modelLowerMaxLostMsgFastVerification ?15 -> modelLowerMaxLostMsg ?16' -> modelNoTransmissionDelayThreat ?21 -> modelLowerSNMax

See at: github.com | CNR ExploRA


2021 Software Unknown

Models and experiments logs for the article published at "Formal Aspects of Computing 2021"
Basile D.
EXPERIMENTS REPRODUCTION PACKAGE This repository contains the models and experiments logs for the article published at Formal Aspects of Computing https://doi.org/10.1007/s00165-021-00556-1 The model.xml contains the model, where all parameters for the set-ups are global, and comments on the queries of the verifier are available to improve readability. Since these comments are not readable by the command-line verifier, the set-up for experiments are in separate files, whose name indicate the specific set-up, among those used in the article, and the indication that these files have been used for the verifyta.exe command-line verifier of Uppaal. In all these set-ups the model is unchanged, but only the specific used parameters. The experiments for the mitigated model, third setup, are also reported in a separate file. In this case, the model has been amended as described in the article. All logs of the execution of experiments are reported. Note that in such logs the probability uncertainty (epsilon) is, in some specific case, different from the one used in the article. We also archived the executable of the used verifier for reproducibility of the logs. A legacy file "model with occ and mitigation.xml" is stored, not useful for reproducibility.

See at: github.com | CNR ExploRA


2021 Software Unknown

Publicity chair tools
Basile D.
This Java app has been developed and used as part of the Publicity Chair role for the Vamos 2022 conference, https://vamos2022.isti.cnr.it/. The application connects through biblioproxy to download a series of publications, identified by their doi, and then processes the pdfs to extract the emails of authors. It is useful to create the list of participants of the last editions of specific conferences, useful for publicity chair purposes.

See at: CNR ExploRA


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

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


2020 Conference article Open Access OPEN

Tackling the Equivalent Mutant Problem in Real-Time Systems: The 12 Commandments of Model-Based Mutation Testing
Basile D., Ter Beek M. H., Cordy M., Legay A.
Mutation testing can effectively drive test generation to reveal faults in software systems. However, it faces a typical efficiency issue as it can produce many mutants that are equivalent to the original system, making it impossible to generate test cases. We consider this problem when model-based mutation testing is applied to real-time system product lines, represented as timed automata. We define novel, time-specific mutation operators and formulate the equivalent mutant problem in the frame of timed refinement relations. Further, we study in which cases a mutation yields an equivalent mutant. Our theoretical results provide guidance to system engineers, allowing them to eliminate mutations from which no test case can be produced. Our evaluation, based on a proof-of-concept tool and an industrial case from the automotive domain, confirms the validity of our theory and demonstrates that our approach can eliminate many of the equivalent mutants (88% in our case study).Source: Proceedings of the 24th International Systems and Software Product Line Conference (SPLC'20), pp. 252–262, Montréal, Québec, Canada, 19-23/10/2020
DOI: 10.1145/3382025.3414966

See at: 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

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

30 years of simulation-based quantitative analysis tools: a comparison experiment between Möbius and Uppaal SMC
Basile D., Ter Beek M. H., Di Giandomenico F., Fantechi A., Gnesi S., Spagnolo G. O.
We provide a brief comparison of the modelling and analysis capabilities of two different formalisms and their associated simulation-based tools, acquired from experimenting with these methods and tools on one specific case study. The case study is a cyber-physical system from an industrial railway project, namely a railroad switch heater, and the quantitative properties concern energy consumption and reliability. We modelled and analysed the case study with stochastic activity networks and Möbius on the one hand and with stochastic hybrid automata and Uppaal SMC on the other hand. We give an overview of the performed experiments and highlight specific features of the two methodologies. This yields some pointers for future research and improvements.Source: ISoLA 2020 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, pp. 368–384, Rhodes, Greece, 20-30/10/2020
DOI: 10.1007/978-3-030-61362-4_21

See at: ISTI Repository Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | doi.org Restricted | 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