-
Chapter and Conference Paper
Trusted Execution Environment for Decentralized Process Mining
Inter-organizational business processes involve multiple independent organizations collaborating to achieve mutual interests. Process mining techniques have the potential to allow these organizations to enhanc...
-
Chapter and Conference Paper
Modelling, Verifying and Testing the Contract Automata Runtime Environment with Uppaal
The contract automata runtime environment (CARE) is a distributed middleware application recently introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we d...
-
Article
Open AccessA toolchain for strategy synthesis with spatial properties
We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools CATLib and VoxLogicA to interact in a fully automated way. The Co...
-
Chapter and Conference Paper
Experimenting with Formal Verification and Model-Based Development in Railways: The Case of UMC and Sparx Enterprise Architect
The use of formal methods can reduce the time and costs associated with railway signalling systems development and maintenance, and improve correct behaviour and safety. The integration of formal methods into ...
-
Chapter and Conference Paper
A Runtime Environment for Contract Automata
Contract automata have been introduced for specifying applications through behavioural contracts and for synthesising their orchestrations as finite state automata. This paper addresses the realisation of appl...
-
Article
Open AccessStatic detection of equivalent mutants in real-time model-based mutation testing
Model-based mutation testing has the potential to effectively drive test generation to reveal faults in software systems. However, it faces a typical efficiency issue since it could produce many mutants that a...
-
Article
Open AccessExploring the ERTMS/ETCS full moving block specification: an experience with formal methods
Shift2Rail is a joint undertaking funded by the EU via its Horizon 2020 program and by main railway stakeholders. Several Shift2Rail projects aim to investigate the application of formal methods to new ERTMS/E...
-
Chapter and Conference Paper
An Experimental Toolchain for Strategy Synthesis with Spatial Properties
We investigate the application of strategy synthesis to enforce spatial properties. The Contract Automata Library (CATLib) performs both composition and strategy synthesis of games modelled in a dialect of finite...
-
Article
Analysing an autonomous tramway positioning system with the Uppaal Statistical Model Checker
The substitution of traditional occupancy detecting sensors with an Autonomous Positioning System (APS) is a promising solution to contain costs and improve performance of current tramway signalling systems. A...
-
Chapter and Conference Paper
Supervisory Synthesis of Configurable Behavioural Contracts with Modalities
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 forma...
-
Chapter and Conference Paper
Formal Analysis of the UNISIG Safety Application Intermediate Sub-layer
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 increas...
-
Chapter and Conference Paper
Enhancing Blockchain-Based Processes with Decentralized Oracles
The automation of business processes via blockchain-based systems allows for trust, reliability and accountability of execution. The link that connects modules that operate within the on-chain sphere and the o...
-
Chapter and Conference Paper
A Clean and Efficient Implementation of Choreography Synthesis for Behavioural Contracts
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...
-
Article
Timed service contract automata
We equip a recently developed model for the specification of service contracts with real-time constraints. Service contracts offer a means to define the behavioural compliance of a composition of services, typ...
-
Chapter and Conference Paper
Strategy Synthesis for Autonomous Driving in a Moving Block Railway System with Uppaal Stratego
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 ...
-
Chapter and Conference Paper
30 Years of Simulation-Based Quantitative Analysis Tools: A Comparison Experiment Between Möbius and Uppaal SMC
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...
-
Chapter and Conference Paper
Designing a Demonstrator of Formal Methods for Railways Infrastructure Managers
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 ...
-
Article
Applying supervisory control synthesis to priced featured automata and energy problems
Software Product Line Engineering (SPLE) promotes extensive reuse of common aspects in develo** new software components. Supervisory Control Theory (SCT) is a methodology to automatically synthesise a contro...
-
Chapter and Conference Paper
Statistical Model Checking of Hazards in an Autonomous Tramway Positioning System
One promising option to improve performance and contain costs of current tramway signalling systems is to introduce an Autonomous Positioning System (APS) in substitution of traditional occupancy detecting sen...
-
Chapter and Conference Paper
The SISTER Approach for Verification and Validation: A Lightweight Process for Reusable Results
The research project SISTER aims to improve the safety and autonomy of light rail trains by develo** and integrating novel technologies for remote sensing and object detection, safe positioning, and broadban...
