20 Result(s)
-
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...
-
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...
-
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 ...
-
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...
-
Chapter
Automata-Based Behavioural Contracts with Action Correlation
The rigorous design of Service-Oriented Computing (SOC) applications has been identified as one of the primary research challenges for the next 10 years. Many foundational theories for SOC have been defined, ...
-
Chapter and Conference Paper
Bridging the Gap Between Supervisory Control and Coordination of Services: Synthesis of Orchestrations and Choreographies
We explore the frontiers between coordination and control systems by discussing a number of contributions to bridging the gap between supervisory control theory and coordination of services
-
Chapter and Conference Paper
Modelling and Analysing ERTMS L3 Moving Block Railway Signalling with Simulink and Uppaal SMC
Efficient and safe railway signalling systems, together with energy-saving infrastructures, are among the main pillars to guarantee sustainable transportation. ERTMS L3 moving block is one of the next generati...
-
Chapter and Conference Paper
Survey on Formal Methods and Tools in Railways: The ASTRail Approach
Formal methods and tools have been widely applied to the development of railway systems during the last decades. However, no universally accepted formal framework has emerged, and railway companies wishing to ...
-
Chapter
A Refined Framework for Model-Based Assessment of Energy Consumption in the Railway Sector
Awareness and efforts to moderate energy consumption, desirable from both economical and environmental perspectives, are nowadays increasingly pursued. However, when critical sectors are addressed, energy savi...
-
Chapter and Conference Paper
On the Industrial Uptake of Formal Methods in the Railway Domain
The railway sector has seen a large number of successful applications of formal methods and tools. However, up-to-date, structured information about the industrial usage and needs related to formal tools in ra...
-
Chapter and Conference Paper
Statistical Model Checking of a Moving Block Railway Signalling Scenario with Uppaal SMC
We present an experience in modelling and statistical model checking a satellite-based moving block signalling scenario from the railway industry with Uppaal SMC. This demonstrates the usability and applicability...
-
Chapter and Conference Paper
Orchestration Synthesis for Real-Time Service Contracts
Service contracts offer a way to define the desired behavioural compliance of a composition of services, characterised by the fulfilment of all requirements (e.g. service requests) by obligations (e.g. service...
-
Chapter and Conference Paper
Dependable Dynamic Routing for Urban Transport Systems Through Integer Linear Programming
Highly automated transport systems play an important role in the transformation towards a digital society, and planning the optimal routes for a set of fleet vehicles has been proved useful for improving the d...
-
Chapter and Conference Paper
Tuning Energy Consumption Strategies in the Railway Domain: A Model-Based Approach
Cautious usage of energy resources is gaining great attention nowadays, both from environmental and economical point of view. Therefore, studies devoted to analyze and predict energy consumption in a variety o...
-
Chapter and Conference Paper
Playing with Our CAT and Communication-Centric Applications
We describe CAT, a toolkit supporting the analysis of communication-centric applications, i.e., applications consisting of ensembles of interacting services. Services are modelled in CAT as contract automata and ...
-
Chapter and Conference Paper
Stochastic Model-Based Analysis of Energy Consumption in a Rail Road Switch Heating System
Rail road switches enable trains to be guided from one track to another, and rail road switches heaters are used to avoid the formation of snow and ice during the cold season in order to guarantee their correc...
-
Chapter
Safe Adaptation Through Implicit Effect Coercion
Context-Oriented programming languages provide us with primitive constructs to adapt programs behaviour depending on the evolution of their operational environment. In this paradigm developers must provide beh...
