Typology
operator:
and / or
Language
operator:
and / or
Date
operator:
and / or
Rights
operator:
and / or
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.
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
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
2017
Software
Unknown
AMPL model for the dependable dynamic vehicle routing problem
Basile D.
AMPL integer linear programming program for the dependable dynamic vehicle routing problem, referred in the paper published at RSSRail 2017
Basile D.
AMPL integer linear programming program for the dependable dynamic vehicle routing problem, referred in the paper published at RSSRail 2017
See at: github.com | CNR ExploRA
2019
Software
Unknown
The Uppaal SMC model and experiments published at RSSRail 2019
Basile D.
The Uppaal SMC model and experiments published at RSSRail 2019 https://link.springer.com/chapter/10.1007%2F978-3-030-18744-6_3
Basile D.
The Uppaal SMC model and experiments published at RSSRail 2019 https://link.springer.com/chapter/10.1007%2F978-3-030-18744-6_3
See at: CNR ExploRA
2023
Software
Unknown
Experimenting with formal verification and model-based development in railways: the case of UMC and Sparx Enterprise Architect - Complementary data
Basile D., Mazzanti F., Ferrari A.
This repository contains the UMC and SPARX EA data used in the paper: Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect by Davide Basile, Franco Mazzanti and Alessio Ferrari.DOI: 10.5281/zenodo.7920448
Project(s): 4SECURAIL
Metrics:
Basile D., Mazzanti F., Ferrari A.
This repository contains the UMC and SPARX EA data used in the paper: Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect by Davide Basile, Franco Mazzanti and Alessio Ferrari.DOI: 10.5281/zenodo.7920448
Project(s): 4SECURAIL
Metrics:
See at: CNR ExploRA
2021
Journal article
Open Access
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
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
See at:
ercim-news.ercim.eu 
| ISTI Repository | ISTI Repository | CNR ExploRA
2020
Other
Unknown
4SECURail video presentation of Sparx EA and demonstrator of formal methods
Basile D.
The formal methods demonstrator of Deliverable 2.2 comprises also a video presentation of the tools and artifacts developed during the project, this is the Sparx EA video.Project(s): 4SECURAIL
Basile D.
The formal methods demonstrator of Deliverable 2.2 comprises also a video presentation of the tools and artifacts developed during the project, this is the Sparx EA video.Project(s): 4SECURAIL
See at: CNR ExploRA | zenodo.org
2020
Software
Unknown
4SECURail D 2.2: Sparx EA artifacts and technical documentation
Basile D.
This is the model, generated source code, exported xmi model, and technical report of the Communication Supervision Layer of the UNISIG Subset 98 developed with Sparx Enterprise Architect for the Deliverable 2.2 of the 4SECURail projectProject(s): 4SECURAIL
Basile D.
This is the model, generated source code, exported xmi model, and technical report of the Communication Supervision Layer of the UNISIG Subset 98 developed with Sparx Enterprise Architect for the Deliverable 2.2 of the 4SECURail projectProject(s): 4SECURAIL
See at: CNR ExploRA | zenodo.org
2016
Software
Unknown
The Stochastic Activity Network models of the rail road switch heating system for Moebius tool
Basile D.
The SAN models of the rail road switch heating system This is a SAN model done in Moebius in 2015 and published at JRTPM2016 https://doi.org/10.1016/j.jrtpm.2016.03.003
Basile D.
The SAN models of the rail road switch heating system This is a SAN model done in Moebius in 2015 and published at JRTPM2016 https://doi.org/10.1016/j.jrtpm.2016.03.003
See at: github.com | CNR ExploRA
2020
Software
Unknown
Stratego formal models and experiments for the paper published at FORTE2020
Basile D.
This is the Uppaal Stratego model published at FORTE2020 https://link.springer.com/chapter/10.1007%2F978-3-030-50086-3_1
Basile D.
This is the Uppaal Stratego model published at FORTE2020 https://link.springer.com/chapter/10.1007%2F978-3-030-50086-3_1
See at: github.com | CNR ExploRA
2021
Software
Unknown
Experiments reproducibility package for the paper static detection of equivalent mutants in real-time model-based mutation testing: an empirical evaluation
Basile D.
This is the experiments reproducibility package for the paper accepted at Empirical Software Engineering (EMSE): "Static Detection of Equivalent Mutants in Real-Time Model-based Mutation Testing: An Empirical Evaluation", Davide Basile, Maurice H. ter Beek, Sami Lazreg, Maxime Cordy and Axel Legay. https://doi.org/10.1007/s10664-022-10149-y https://rdcu.be/dilfK This repository contains a video tutorial for reproducing the experiments.DOI: 10.5281/zenodo.5749731
Metrics:
Basile D.
This is the experiments reproducibility package for the paper accepted at Empirical Software Engineering (EMSE): "Static Detection of Equivalent Mutants in Real-Time Model-based Mutation Testing: An Empirical Evaluation", Davide Basile, Maurice H. ter Beek, Sami Lazreg, Maxime Cordy and Axel Legay. https://doi.org/10.1007/s10664-022-10149-y https://rdcu.be/dilfK This repository contains a video tutorial for reproducing the experiments.DOI: 10.5281/zenodo.5749731
Metrics:
See at: CNR ExploRA
2023
Contribution to conference
Open Access
Research challenges in orchestration synthesis
Basile D.
This is the presentation of the paper "Research Challenges in Orchestration Synthesis" by Davide Basile and Maurice H. ter Beek, presented at the 16th Interaction and Concurrency Experience satellite workshop of the 18th International Federated Conference on Distributed Computing Techniques (DisCoTec 2023).Source: DisCoTec 2023 - 43rd IFIP WG 6.1 International Conference, FORTE 2023 Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, Lisbon, Portugal, 19-23/06/2023
Basile D.
This is the presentation of the paper "Research Challenges in Orchestration Synthesis" by Davide Basile and Maurice H. ter Beek, presented at the 16th Interaction and Concurrency Experience satellite workshop of the 18th International Federated Conference on Distributed Computing Techniques (DisCoTec 2023).Source: DisCoTec 2023 - 43rd IFIP WG 6.1 International Conference, FORTE 2023 Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, Lisbon, Portugal, 19-23/06/2023
See at:
ISTI Repository | youtu.be | CNR ExploRA
2023
Contribution to conference
Open Access
Experimenting with formal verification and model-based development: the case of UMC and Sparx EA
Basile D.
This is the presentation of "Experimenting with Formal Verification and Model-Based Development in Railways: The Case of UMC and Sparx Enterprise Architect" by Davide Basile, Franco Mazzanti, Alessio Ferrari, Presented at the 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20-22, 2023. https://doi.org/10.1007/978-3-031-43681-9_1Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, Antwerp, Belgium, 20-22/09/2023
Basile D.
This is the presentation of "Experimenting with Formal Verification and Model-Based Development in Railways: The Case of UMC and Sparx Enterprise Architect" by Davide Basile, Franco Mazzanti, Alessio Ferrari, Presented at the 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20-22, 2023. https://doi.org/10.1007/978-3-031-43681-9_1Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, Antwerp, Belgium, 20-22/09/2023
See at:
ISTI Repository | www.youtube.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.
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
2023
Contribution to conference
Open Access
A runtime environment for contract automata
Basile D.
This is the presentation of the paper "A Runtime Environment for Contract Automata", published at the 25th International Symposium on Formal Methods. The paper is available at https://doi.org/10.1007/978-3-031-27481-7_31Source: FM 2023 - Formal Methods: 25th International Symposium, Luebeck, Germany, 6-10/03/2023
Basile D.
This is the presentation of the paper "A Runtime Environment for Contract Automata", published at the 25th International Symposium on Formal Methods. The paper is available at https://doi.org/10.1007/978-3-031-27481-7_31Source: FM 2023 - Formal Methods: 25th International Symposium, Luebeck, Germany, 6-10/03/2023
See at:
ISTI Repository | youtu.be | CNR ExploRA
2022
Software
Unknown
Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods - Complementary data
Basile D.
This repository contains the models for the paper, created with Uppaal SMC version 4.1.19 and 4.1.24 (http://www.uppaal.org/). Basile, D., ter Beek, M.H., Ferrari, A. and Legay, A., 2022. Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods. International Journal on Software Tools for Technology Transfer, 24(3), pp.351-370. https://doi.org/10.1007/s10009-022-00653-3DOI: 10.5281/zenodo.8207726
Project(s): ASTRail
Metrics:
Basile D.
This repository contains the models for the paper, created with Uppaal SMC version 4.1.19 and 4.1.24 (http://www.uppaal.org/). Basile, D., ter Beek, M.H., Ferrari, A. and Legay, A., 2022. Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods. International Journal on Software Tools for Technology Transfer, 24(3), pp.351-370. https://doi.org/10.1007/s10009-022-00653-3DOI: 10.5281/zenodo.8207726
Project(s): ASTRail
Metrics:
See at: CNR ExploRA
2023
Software
Unknown
Modelling, verifying and testing the contract automata runtime environment with Uppaal: complementary data
Basile D.
This repository contains the complementary material for the paper: "Modelling and Verifying the Contract Automata Runtime Environment", Basile D. The latest version of the included files can be accessed through the GitHub repository of the Contract Automata Runtime Environment, https://github.com/contractautomataproject/CARE/tree/master/src/spec/uppaal In addition to the other contents, this Zenodo repository contains all the logs of the experiments.
Basile D.
This repository contains the complementary material for the paper: "Modelling and Verifying the Contract Automata Runtime Environment", Basile D. The latest version of the included files can be accessed through the GitHub repository of the Contract Automata Runtime Environment, https://github.com/contractautomataproject/CARE/tree/master/src/spec/uppaal In addition to the other contents, this Zenodo repository contains all the logs of the experiments.
See at: CNR ExploRA | zenodo.org
2021
Master thesis
Open Access
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
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
See at:
ISTI Repository | sol.unifi.it 
| CNR ExploRA
2020
Journal article
Open Access
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).
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 | ISTI Repository | CNR ExploRA
2019
Software
Unknown
The Uppaal SMC models developed for the ASTRail project and experiments, published at Isola2018 and FMICS2019
Basile D.
This repository contains various models of the ERTMS ETCS L3 Moving Block specification (https://en.wikipedia.org/wiki/European_Train_Control_System#Level_3), with increasing level of details, that stem from the ASTRail project (http://www.astrail.eu/) and the Deliverable 5.1 of X2Rail1 project (https://projects.shift2rail.org/X2RAIL-1), created with Uppaal SMC version 4.1.19 and 4.1.24 (http://www.uppaal.org/). The models and analyses have been published in Isola2018 and FMICS2019.Project(s): ASTRail
Basile D.
This repository contains various models of the ERTMS ETCS L3 Moving Block specification (https://en.wikipedia.org/wiki/European_Train_Control_System#Level_3), with increasing level of details, that stem from the ASTRail project (http://www.astrail.eu/) and the Deliverable 5.1 of X2Rail1 project (https://projects.shift2rail.org/X2RAIL-1), created with Uppaal SMC version 4.1.19 and 4.1.24 (http://www.uppaal.org/). The models and analyses have been published in Isola2018 and FMICS2019.Project(s): ASTRail
See at: github.com | CNR ExploRA