2023
Other
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).
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).
See at:
CNR IRIS 
| ISTI Repository | youtu.be | CNR IRIS 
| CNR IRIS
2021
Software
Open Access
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 IRIS | CNR IRIS
2021
Software
Open Access
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 IRIS | CNR IRIS
2017
Software
Open Access
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 IRIS | CNR IRIS
2019
Software
Restricted
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
2023
Software
Metadata Only Access
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 IRIS
2023
Other
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_1
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_1
See at:
CNR IRIS | ISTI Repository | www.youtube.com | CNR IRIS | CNR IRIS
2024
Other
Open Access
Presentation of the paper entitled Modelling, Verifying and Testing the Contract Automata Runtime Environment with UPPAAL
Davide Basile
This is the presentation of the paper entitled "Modelling, Verifying and Testing the Contract Automata Runtime Environment with Uppaal" by Davide Basile, presented at Coordination Models and Languages - 26th IFIP WG 6.1 International Conference, COORDINATION 2024, Held as Part of the 19th International Federated Conference on Distributed Computing Techniques, DisCoTec 2024, Groningen, The Netherlands, June 17-21, 2024, https://doi.org/10.1007/978-3-031-626...Project(s): ADVancEd iNtegraTed evalUation of Railway systEms
Davide Basile
This is the presentation of the paper entitled "Modelling, Verifying and Testing the Contract Automata Runtime Environment with Uppaal" by Davide Basile, presented at Coordination Models and Languages - 26th IFIP WG 6.1 International Conference, COORDINATION 2024, Held as Part of the 19th International Federated Conference on Distributed Computing Techniques, DisCoTec 2024, Groningen, The Netherlands, June 17-21, 2024, https://doi.org/10.1007/978-3-031-626...Project(s): ADVancEd iNtegraTed evalUation of Railway systEms
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, vol. 2021 (issue 126), pp. 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, vol. 2021 (issue 126), pp. 32-33
Project(s): 4SECURAIL
See at:
ercim-news.ercim.eu | CNR IRIS | ISTI Repository | ISTI Repository | CNR IRIS | CNR IRIS
2020
Other
Metadata Only Access
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 IRIS | zenodo.org
2020
Software
Open Access
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 IRIS | zenodo.org | CNR IRIS | CNR IRIS | CNR IRIS
2016
Software
Open Access
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 IRIS | CNR IRIS
2020
Software
Open Access
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 IRIS | CNR IRIS
2023
Other
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_31
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_31
See at:
CNR IRIS | ISTI Repository | youtu.be | CNR IRIS | CNR IRIS
2021
Software
Metadata Only Access
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 IRIS
2021
Software
Open Access
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.
2022
Other
Open Access
A runtime environment for contract automata
Basile D, Ter Beek Mh
Realising contract-based applications from formal specifications with formal guarantees requires to show the adherence of a specification, the contract, to its implementation. Contract automata have been introduced for specifying contract-based applications and synthesising their orchestrations as finite state automata. This paper introduces CARE, a newly developed library for implementing applications specified via contract automata, providing a runtime environment to coordinate services implementing contracts.
Basile D, Ter Beek Mh
Realising contract-based applications from formal specifications with formal guarantees requires to show the adherence of a specification, the contract, to its implementation. Contract automata have been introduced for specifying contract-based applications and synthesising their orchestrations as finite state automata. This paper introduces CARE, a newly developed library for implementing applications specified via contract automata, providing a runtime environment to coordinate services implementing contracts.
See at:
arxiv.org | CNR IRIS | ISTI Repository | CNR IRIS
2022
Journal article
Open Access
Contract automata library
Basile D, Ter Beek Mh
Contract automata facilitate the specification, composition, and synthesis of behavioural contracts, comprehending modalities and configurations. Contract automata are supported by a software API called Contract Automata Library. This paper accompanies the software artefact by discussing its architecture, showing some usage examples and presenting recent improvements of the software in terms of quality, availability, usability, and documentation.Source: SCIENCE OF COMPUTER PROGRAMMING, vol. 221 (issue 102841)
DOI: 10.1016/j.scico.2022.102841
Metrics:
Basile D, Ter Beek Mh
Contract automata facilitate the specification, composition, and synthesis of behavioural contracts, comprehending modalities and configurations. Contract automata are supported by a software API called Contract Automata Library. This paper accompanies the software artefact by discussing its architecture, showing some usage examples and presenting recent improvements of the software in terms of quality, availability, usability, and documentation.Source: SCIENCE OF COMPUTER PROGRAMMING, vol. 221 (issue 102841)
DOI: 10.1016/j.scico.2022.102841
Metrics:
See at:
CNR IRIS | ISTI Repository | www.sciencedirect.com | Science of Computer Programming | CNR IRIS | CNR IRIS
2022
Software
Metadata Only Access
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 IRIS
2023
Software
Open Access
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 IRIS | zenodo.org | CNR IRIS