Secure and Unfailing Services. - Davide Basile 001; Pierpaolo Degano; Gian-Luigi Ferrari 002 (PaCT, 2013)

Automata for Analysing Service Contracts. - Davide Basile 001; Pierpaolo Degano; Gian-Luigi Ferrari 002 (TGC, 2014)

From Orchestration to Choreography through Contract Automata. - Davide Basile 001; Pierpaolo Degano; Gian-Luigi Ferrari 002; Emilio Tuosto (ICE, 2014)

A formal framework for secure and complying services. - Davide Basile 001; Pierpaolo Degano; Gian-Luigi Ferrari 002 (J. Supercomput., 2014)

Safe Adaptation Through Implicit Effect Coercion. - Davide Basile 001; Letterio Galletta; Gianluca Mezzetti (Programming Languages with Applications to Biology and Security, 2015)

Stochastic Model-Based Analysis of Energy Consumption in a Rail Road Switch Heating System. - Davide Basile 001; Silvano Chiaradonna; Felicita Di Giandomenico; Stefania Gnesi; Franco Mazzanti (SERENE, 2015)

Playing with Our CAT and Communication-Centric Applications. - Davide Basile 001; Pierpaolo Degano; Gian-Luigi Ferrari 002; Emilio Tuosto (FORTE, 2016)

Tuning Energy Consumption Strategies in the Railway Domain: A Model-Based Approach. - Davide Basile 001; Felicita Di Giandomenico; Stefania Gnesi (ISoLA (2), 2016)

Automata for Specifying and Orchestrating Service Contracts. - Davide Basile 001; Pierpaolo Degano; Gian-Luigi Ferrari 002 (Log. Methods Comput. Sci., 2016)

Relating two automata-based models of orchestration and choreography. - Davide Basile 001; Pierpaolo Degano; Gian-Luigi Ferrari 002; Emilio Tuosto (J. Log. Algebraic Methods Program., 2016)

A stochastic model-based approach to analyse reliable energy-saving rail road switch heating systems. - Davide Basile 001; Silvano Chiaradonna; Felicita Di Giandomenico; Stefania Gnesi (J. Rail Transp. Plan. Manag., 2016)

Specification and Verification of Contract-Based Applications. - Davide Basile 001 (2016)

Enhancing Models Correctness through Formal Verification: A Case Study from the Railway Domain. - Davide Basile 001; Felicita Di Giandomenico; Stefania Gnesi (MODELSWARD, 2017)

Dependable Dynamic Routing for Urban Transport Systems Through Integer Linear Programming. - Davide Basile 001; Felicita Di Giandomenico; Stefania Gnesi (RSSRail, 2017)

Statistical model checking of an energy-saving cyber-physical system in the railway domain. - Davide Basile 001; Felicita Di Giandomenico; Stefania Gnesi (SAC, 2017)

A Refinement Approach to Analyse Critical Cyber-Physical Systems. - Davide Basile 001; Felicita Di Giandomenico; Stefania Gnesi (SEFM Workshops, 2017)

Orchestration of Dynamic Service Product Lines with Featured Modal Contract Automata. - Davide Basile 001; Maurice H. ter Beek; Felicita Di Giandomenico; Stefania Gnesi (SPLC (B), 2017)

FMCAT: Supporting Dynamic Service-based Product Lines. - Davide Basile 001; Felicita Di Giandomenico; Stefania Gnesi (SPLC (B), 2017)

Specifying variability in service contracts. - Davide Basile 001; Felicita Di Giandomenico; Stefania Gnesi; Pierpaolo Degano; Gian-Luigi Ferrari 002 (VaMoS, 2017)

On the Industrial Uptake of Formal Methods in the Railway Domain - A Survey with Stakeholders. - Davide Basile 001; Maurice H. ter Beek; Alessandro Fantechi; Stefania Gnesi; Franco Mazzanti; Andrea Piattino; Daniele Trentini; Alessio Ferrari 001 (IFM, 2018)

Statistical Model Checking of a Moving Block Railway Signalling Scenario with Uppaal SMC - Experience and Outlook. - Davide Basile 001; Maurice H. ter Beek; Vincenzo Ciancia (ISoLA (2), 2018)

Modelling and analysis with featured modal contract automata. - Davide Basile 001; Maurice H. ter Beek; Stefania Gnesi (SPLC (2), 2018)

Orchestration Synthesis for Real-Time Service Contracts. - Davide Basile 001; Maurice H. ter Beek; Axel Legay; Louis-Marie Traonouez (VECoS, 2018)

Automata-Based Behavioural Contracts with Action Correlation. - Davide Basile 001; Rosario Pugliese; Francesco Tiezzi 001; Pierpaolo Degano; Gian-Luigi Ferrari 002 (From Software Engineering to Formal Methods and Tools, and Back, 2019)

A Refined Framework for Model-Based Assessment of Energy Consumption in the Railway Sector. - Silvano Chiaradonna; Felicita Di Giandomenico; Giulio Masetti; Davide Basile 001 (From Software Engineering to Formal Methods and Tools, and Back, 2019)

Bridging the Gap Between Supervisory Control and Coordination of Services: Synthesis of Orchestrations and Choreographies. - Davide Basile 001; Maurice H. ter Beek; Rosario Pugliese (COORDINATION, 2019)

Modelling and Analysing ERTMS L3 Moving Block Railway Signalling with Simulink and Uppaal SMC. - Davide Basile 001; Maurice H. ter Beek; Alessio Ferrari 001; Axel Legay (FMICS, 2019)

Statistical Model Checking of Hazards in an Autonomous Tramway Positioning System. - Davide Basile 001; Alessandro Fantechi; Luigi Rucher; Gianluca Mandò (RSSRail, 2019)

Survey on Formal Methods and Tools in Railways: The ASTRail Approach. - Alessio Ferrari 001; Maurice H. ter Beek; Franco Mazzanti; Davide Basile 001; Alessandro Fantechi; Stefania Gnesi; Andrea Piattino; Daniele Trentini (RSSRail, 2019)

The SISTER Approach for Verification and Validation: A Lightweight Process for Reusable Results. - Andrea Ceccarelli; Davide Basile 001; Andrea Bondavalli; Lorenzo Falai; Alessandro Fantechi; Sandro Ferrari; Gianluca Mandò; Nicola Nostro; Luigi Rucher (SAFECOMP Workshops, 2019)

Applying supervisory control synthesis to priced featured automata and energy problems. - Davide Basile 001 (Int. J. Softw. Tools Technol. Transf., 2019)

Strategy Synthesis for Autonomous Driving in a Moving Block Railway System with Uppaal Stratego. - Davide Basile 001; Maurice H. ter Beek; Axel Legay (FORTE, 2020)

Comparing formal tools for system design: a judgment study. - Alessio Ferrari 001; Franco Mazzanti; Davide Basile 001; Maurice H. ter Beek; Alessandro Fantechi (ICSE, 2020)

Designing a Demonstrator of Formal Methods for Railways Infrastructure Managers. - Davide Basile 001; Maurice H. ter Beek; Alessandro Fantechi; Alessio Ferrari 001; Stefania Gnesi; Laura Masullo; Franco Mazzanti; Andrea Piattino; Daniele Trentini (ISoLA (3), 2020)

30 Years of Simulation-Based Quantitative Analysis Tools: A Comparison Experiment Between Möbius and Uppaal SMC. - Davide Basile 001; Maurice H. ter Beek; Felicita Di Giandomenico; Alessandro Fantechi; Stefania Gnesi; Giorgio Oronzo Spagnolo (ISoLA (1), 2020)

Tackling the equivalent mutant problem in real-time systems: the 12 commandments of model-based mutation testing. - Davide Basile 001; Maurice H. ter Beek; Maxime Cordy; Axel Legay (SPLC (A), 2020)

A Formal Methods Demonstrator for Railways. - Franco Mazzanti; Davide Basile 001 (ERCIM News, 2020)

Timed service contract automata. - Davide Basile 001; Maurice H. ter Beek; Axel Legay (Innov. Syst. Softw. Eng., 2020)

Synthesis of Orchestrations and Choreographies: Bridging the Gap between Supervisory Control and Coordination of Services. - Davide Basile 001; Maurice H. ter Beek; Rosario Pugliese (Log. Methods Comput. Sci., 2020)

Controller synthesis of service contracts with variability. - Davide Basile 001; Maurice H. ter Beek; Pierpaolo Degano; Axel Legay; Gian-Luigi Ferrari 002; Stefania Gnesi; Felicita Di Giandomenico (Sci. Comput. Program., 2020)

A Clean and Efficient Implementation of Choreography Synthesis for Behavioural Contracts. - Davide Basile 001; Maurice H. ter Beek (COORDINATION, 2021)

Formal Analysis of the UNISIG Safety Application Intermediate Sub-layer - Applying Formal Methods to Railway Standard Interfaces. - Davide Basile 001; Alessandro Fantechi; Irene Rosadi (FMICS, 2021)

Supervisory Synthesis of Configurable Behavioural Contracts with Modalities. - Davide Basile 001; Maurice H. ter Beek; Pierpaolo Degano; Axel Legay; Gian-Luigi Ferrari 002; Stefania Gnesi; Felicita Di Giandomenico (FORTE, 2021)

Systematic Evaluation and Usability Analysis of Formal Tools for Railway System Design. - Alessio Ferrari 001; Franco Mazzanti; Davide Basile 001; Maurice H. ter Beek (CoRR, 2021)

Secure Multi-Party Computation with Service Contract Automata. - Davide Basile 001 (ERCIM News, 2021)

Analysing an autonomous tramway positioning system with the Uppaal Statistical Model Checker. - Davide Basile 001; Alessandro Fantechi; Luigi Rucher; Gianluca Mandò (Formal Aspects Comput., 2021)

Systematic Evaluation and Usability Analysis of Formal Tools for Railway System Design - Technical Annexes. - Franco Mazzanti; Alessio Ferrari 001; Davide Basile 001; Maurice H. ter Beek (Zenodo, 2021)

Systematic Evaluation and Usability Analysis of Formal Tools for Railway System Design - Technical Annexes. - Franco Mazzanti; Alessio Ferrari 001; Davide Basile 001; Maurice H. ter Beek (Zenodo, 2021)

Systematic Evaluation and Usability Analysis of Formal Tools for Railway System Design - Technical Annexes. - Franco Mazzanti; Alessio Ferrari 001; Davide Basile 001; Maurice H. ter Beek (Zenodo, 2021)

An Experimental Toolchain for Strategy Synthesis with Spatial Properties. - Davide Basile 001; Maurice H. ter Beek; Vincenzo Ciancia (ISoLA (3), 2022)

Empirical Software Engineering and Formal Methods for IoT Systems. - Davide Basile 001; Maurice H. ter Beek; Giovanna Broccia; Alessio Ferrari 001 (ERCIM News, 2022)

Static detection of equivalent mutants in real-time model-based mutation testing. - Davide Basile 001; Maurice H. ter Beek; Sami Lazreg; Maxime Cordy; Axel Legay (Empir. Softw. Eng., 2022)

Contract Automata Library. - Davide Basile 001; Maurice H. ter Beek (Sci. Comput. Program., 2022)

Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods. - Davide Basile 001; Maurice H. ter Beek; Alessio Ferrari 001; Axel Legay (Int. J. Softw. Tools Technol. Transf., 2022)

Systematic Evaluation and Usability Analysis of Formal Methods Tools for Railway Signaling System Design. - Alessio Ferrari 001; Franco Mazzanti; Davide Basile 001; Maurice H. ter Beek (IEEE Trans. Software Eng., 2022)

A Runtime Environment for Contract Automata. - Davide Basile 001; Maurice H. ter Beek (FM, 2023)

Experimenting with Formal Verification and Model-Based Development in Railways: The Case of UMC and Sparx Enterprise Architect. - Davide Basile 001; Franco Mazzanti; Alessio Ferrari 001 (FMICS, 2023)

Mutant Equivalence as Monotonicity in Parametric Timed Games. - Davide Basile 001; Maurice H. ter Beek; Hendrik Göttmann; Malte Lochau (FormaliSE, 2023)

Research Challenges in Orchestration Synthesis. - Davide Basile 001; Maurice H. ter Beek (ICE, 2023)

A Sound and Complete Refinement Relation for Non-reducible Modal Transition Systems. - Davide Basile 001 (CoRR, 2023)

A Toolchain for Strategy Synthesis with Spatial Properties - Complementary Material. - Davide Basile 001; Maurice H. ter Beek; Laura Bussi; Vincenzo Ciancia (Zenodo, 2023)

A toolchain for strategy synthesis with spatial properties. - Davide Basile 001; Maurice H. ter Beek; Laura Bussi; Vincenzo Ciancia (Int. J. Softw. Tools Technol. Transf., 2023)

Modelling, Verifying and Testing the Contract Automata Runtime Environment with Uppaal. - Davide Basile 001 (COORDINATION, 2024)

Time for Networks: Mutation Testing for Timed Automata Networks. - David Cortés; James Ortiz 001; Davide Basile 001; Jesús Aranda; Gilles Perrouin; Pierre-Yves Schobbens (FormaliSE@ICSE, 2024)

An Integrated Perspective on the Evaluation of Complex Railway Systems. - Davide Basile 001; Maurice H. ter Beek; Laura Carnevali; Silvano Chiaradonna; Felicita Di Giandomenico; Alessandro Fantechi; Gloria Gori (ISoLA (5), 2024)

Sustainable Mobility: Increase of Capacity and Digitisation of Railway Transport. - Davide Basile 001; Maurice H. ter Beek; Alessio Ferrari 001 (ERCIM News, 2024)

Advanced Integrated Evaluation of Railway Systems . - Davide Basile 001; Maurice H. ter Beek; Felicita Di Giandomenico; Laura Carnevali; Alessandro Fantechi (ERCIM News, 2024)

Advancing orchestration synthesis for contract automata. - Davide Basile 001; Maurice H. ter Beek (J. Log. Algebraic Methods Program., 2024)

Coherent modal transition systems refinement. - Davide Basile 001; Maurice H. ter Beek; Alessandro Fantechi; Stefania Gnesi (J. Log. Algebraic Methods Program., 2024)

Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing. - Davide Basile 001 (CoRR, 2025)