Large-scale synthetic environments are essential for advancing smart cities research. However, existing urban benchmarks typically prioritize either visual photorealism or geometric fidelity, often neglecting the material-level semantics and physical attributes required for simulations. To address this gap, this paper introduces UR-MAT , a modular design framework and a multimodal synthetic dataset specifically built to bridge computer vision and physics-based modelling. We present a unified construction workflow that integrates georeferenced geometry, physically based rendering (PBR) materials, and domain-specific metadata (e.g., electromagnetic properties based on ITU-R standards) into a traceable data representation. The resulting dataset encompasses eight heterogeneous urban scenarios, providing spatially aligned RGB imagery, depth maps, semantic segmentation masks, and 3D point clouds. The utility of UR-MAT is validated through cross-domain experiments: (i) a quantitative baseline analysis on semantic material segmentation across fourteen material classes, where the best-performing model achieved 0.787 mIoU and 0.968 pixel accuracy, and (ii) electromagnetic ray-tracing simulations, which verify that the dataset’s material annotations yield physically consistent and deterministic radio propagation patterns. By enabling perception and simulation tasks within a single coherent framework, UR-MAT serves as a resource for developing perception-driven communication strategies and next-generation Digital Twins.

The development of smart city applications increasingly relies on datasets that capture not only urban geometry but also the material properties that influence real-world interactions. However, most existing datasets lack detailed semantic labels and physical attributes, limiting their applicability to tasks such as signal propagation modeling and material-aware analysis. In this paper, we propose a structured process and a tool pipeline for generating material-aware synthetic datasets from custom 3D urban scenes. Our approach integrates 3D modeling, physically-based rendering, and automated data capture to produce multimodal outputs, including RGB images, depth maps, segmentation masks, structured metadata, and annotated 3D meshes. We demonstrate the process and pipeline instantiation using the Louvre Museum district as a running scenario, capturing the site's complex architecture and material diversity. A preliminary ray-tracing simulation in MATLAB further demonstrates how the generated data can support material-aware applications. By bridging geometry, appearance, and physical information, the proposed solution can contribute to advancing simulation-ready datasets for smart city research.

We present UR-MAT, a multimodal, material-aware synthetic dataset for urban scene understanding and physics-based simulation. UR-MAT comprises seven diverse outdoor environments, ranging from historic districts to modern office areas, reconstructed from OpenStreetMap data and procedurally enhanced in Unreal Engine. Each scene includes semantically structured 3D meshes and physically based rendering (PBR) materials annotated with electromagnetic properties such as permittivity, reflectance, and attenuation. The dataset provides spatially aligned RGB images, material segmentation masks, depth maps, point clouds, camera poses, and 3D mesh files in .glb format. All data is generated through a deterministic, reproducible pipeline integrating OSM2World, Unreal Engine, and UnrealCV. UR-MAT supports a wide range of research tasks, from semantic segmentation and 3D reconstruction to material-aware electromagnetic simulation (e.g., mmWave propagation). We also release two utility scripts to extract mesh-material relationships and assign physical metadata, enabling dataset extension and reproducibility. By bridging computer vision and physical modeling, UR-MAT serves as a testbed for multimodal AI and signal-aware urban simulation.

Level Crossings are among the most critical railway assets, concerning both the risk of accidents and their maintainability, due to intersections with promiscuous traffic and difficulties in remotely monitoring their health status. Failures can be originated from several factors, including malfunctions in the bar mechanisms and warning devices, such as light signals and bells. This paper focuses on the intelligent detection of anomalies in warning bells through non-intrusive acoustic monitoring by: (1) introducing a new concept for autonomous monitoring of level crossings; (2) generating and sharing a specific dataset collecting relevant audio signals from publicly available audio recordings; (3) implementing and evaluating a solution combining deep learning and transfer learning for warning bell detection. The results show a high accuracy in detecting anomalies and suggest viability of the approach in real-world applications, especially where network cameras with on-board microphones are installed for multi-purpose level crossing surveillance.

Abstract The emergence of 5G technologies opens up new opportunities for railway communications. One of the foundational aspects of 5G architecture is its control-plane programmability, which can be achieved through Software Defined Networking (SDN). In railway scenarios, this can be used to dynamically reconfigure the network for a more effective and efficient management of communication flows produced by moving trains. The paper presents a framework for integrating modelling and analysis tools into a programmable control plane specifically tailored to railway communications. We introduce the concept of domain-awareness in the network control plane as an SDN-enabled feature that allows achieving application-specific advantages besides those purely expressed in terms of key performance indicators such as the quality of service. We propose a reference architecture in which domain-awareness in the control plane is obtained by considering information gathered by network devices and ad-hoc communication gateways that are able to detect relevant signalling events. In the architecture, the actual behaviour of the SDN controller is governed by applications that are able to react to specific triggers and re-configure network devices accordingly. We also provide a methodological framework based on model-driven engineering and formal methods, including dynamic state machines, for the automatic generation of SDN control plane logic.

Artificial Intelligence (AI) is becoming pervasive in most engineering domains, and railway transport is no exception. However, due to the plethora of different new terms and meanings associated with them, there is a risk that railway practitioners, as several other categories, will get lost in those ambiguities and fuzzy boundaries, and hence fail to catch the real opportunities and potential of machine learning, artificial vision, and big data analytics, just to name a few of the most promising approaches connected to AI. The scope of this paper is to introduce the basic concepts and possible applications of AI to railway academics and practitioners. To that aim, this paper presents a structured taxonomy to guide researchers and practitioners to understand AI techniques, research fields, disciplines, and applications, both in general terms and in close connection with railway applications such as autonomous driving, maintenance, and traffic management. The important aspects of ethics and explainability of AI in railways are also introduced. The connection between AI concepts and railway subdomains has been supported by relevant research addressing existing and planned applications in order to provide some pointers to promising directions.

Abstract The current travel demand in railways requires the adoption of novel approaches and technologies in order to increase network capacity. Virtual Coupling is considered one of the most innovative solutions to increase railway capacity by drastically reducing train headway. The aim of this paper is to provide an approach to investigate the potential of Virtual Coupling in railways by composing stochastic activity networks model templates. The paper starts describing the Virtual Coupling paradigm with a focus on standard European railway traffic controllers. Based on stochastic activity network model templates, we provide an approach to perform quantitative evaluation of capacity increase in reference Virtual Coupling scenarios. The approach can be used to estimate system capacity over a modelled track portion, accounting for the scheduled service as well as possible failures. Due to its modularity, the approach can be extended towards the inclusion of safety model components. The contribution of this paper is a preliminary result of the PERFORMINGRAIL (PERformance-based Formal modelling and Optimal tRaffic Management for movING-block RAILway signalling) project funded by the European Shift2Rail Joint Undertaking.

Railway infrastructure operators need to push their network capacity up to their limits in high-traffic corridors. Virtual coupling is considered among the most relevant innovations to be studied within the European Horizon 2020 Shift2Rail Joint Undertaking as it can drastically reduce headways and thus increase the line capacity by allowing to dynamically connect two or more trains in a single convoy. This paper provides a proof of concept of Virtual coupling by introducing a specific operating mode within the European rail traffic management system/European train control system (ERTMS/ETCS) standard specification, and by defining a coupling control algorithm accounting for time-varying delays affecting the communication links. To that aim, we define one ploy to enrich the ERTMS/ETCS with Virtual coupling without changing its working principles and we borrow a numerical analysis methodology used to study platooning in the automotive field. The numerical analysis is also provided to support the proof of concept with quantitative results in a case-study simulation scenario.

Model-driven techniques can be used to automatically produce formal models from different views of a system realised by using several modelling languages and notations. Specifications are transformed into formal models so facilitating the analysis of complex system for design, validation or verification purposes. However, no single formalism suits for representing all system’s views. In particular, the assessment of non-functional properties often requires integrated modelling approaches. The ultimate goal of the research work described in this paper is to develop a comprehensive, theoretical and practical framework able to support the development and the integration of new or existing model-driven approaches for the automatic generation of multi-formalism models. This paper defines the core theoretical ideas on which the framework is based and demonstrates their concrete applicability to the development of a multi-formalism approach for performability assessment.

This paper aims at defining a model-driven approach for the diagnosability analysis of discrete event systems (DES). The proposed approach can be adopted during the design of modern control systems, in which many sensors and actuators are employed and the diagnosability of faults within a certain delay could be an issue. The proposal represents a first step towards an automatic model-driven process which derive formal models from a complete high-level specification of DESs. The specification activity of our approach relies on the Dynamic STate Machine (DSTM) formalism, a new language that extends state machines with dynamic instantiation, interrupts and asynchronous communication. The paper will describe how we can automatically derive Petri net and Promela models from the high-level DSTM specification. The former model can be used to apply diagnosability analysis approaches proposed in the DES community, while the latter can be used to apply model checking techniques. An application of the proposed model-driven approach is described by deriving both a PN and a Promela model for the well-known railway level crossing benchmark.

The development and analysis of increasingly complex systems require the intensive use of models and of sophisticated approaches to systems modeling. This paper focuses on workflows supporting the solution of complex, composed, formal models used to study and/or develop real-world systems. The workflows we deal with orchestrate multiple distributed tools and applications in order to provide the user with a powerful, composed solution environment. The aim is to automate and reproduce analysis and simulation tasks starting from a high level, graph-based description of the model to be solved. This paper thus introduces solution workflows and presents the Solution Process Definition Language (SPDL) for the specification of solution workflows processes. One of the key elements of SPDL is its formal semantics, which allow for unambiguous specification of its constructs and validation of the workflows. A workflow pattern analysis of SPDL is also provided. SPDL and its execution environment, the OsMoSys framework, are then applied to a homeland security scenario. The OsMoSys framework and the SPDL language provide a practical contribution to the applicability of model engineering techniques by enabling the semiautomatic solution of complex models.

The security of railway and mass-transit systems is increasingly dependant on the effectiveness of integrated Security Management Systems (SMS), which are meant to detect threats and to provide operators with information required for alarm verification purposes. In order to lower the false alarm rate and improve the detection reliability of threat scenarios, event correlation capabilities need to be integrated into the SMS. In this paper an existing approach based on a-priori defined event patterns is extended using a heuristic situation recognition approach which is more robust to both imperfect scenario modeling (human faults) and missed detections (sensor faults). The approach is based on similarity analysis between the event trees representing scenarios and it is effective both on-line and off-line. Applied on-line, it allows for an earlier and more fault-tolerant threat detection, since scenario matching is not required to be complete nor exact. Applied off-line, its effectiveness is twofold: first, it allows for detecting redundancies when updating the scenario repository; secondly, it enhances the post-event forensic search of suspicious behaviors not previously stored in the scenario repository. The strategy is being experimented in the context of railway protection.

A common approach to formally describe security mechanisms is the definition of proper policies. In many contexts, a system could be considered secure and trustworthy if the policy enforced by its security administrator is trust-worthy as well; within such contexts it is possible to evaluate the system security by evaluating its policy. In a previous paper we have proposed a policy-based methodology, the reference evaluation methodology (REM for short), to define and evaluate the security level that a system is able to provide. In this paper we illustrate the implementation of the REM framework to automatically evaluate the security level provided by a system and we discuss a real case study on the evaluation of the Certificate Authorities involved in the EUGridPMA project.

Composition of web services is of great interest to support business-to-business collaboration and provide value added services with desired properties or capabilities. Nevertheless, the standard languages used to create business processes from composite web services lack of formal definition of their semantics and tools to support the analysis of a business process. In this paper we provide a practical approach to formal verification of BPEL4WS executable processes. A syntax-driven operational semantics for BPEL4WS is introduced and an automatic verifier is presented in order to perform a semantic analysis of the flow constructs used in the definition of BPEL4WS processes.

The security of complex infrastructures depends on many technical and organizational issues that need to be properly addressed by a security policy. For purpose of our discussion, we define a security policy as a document that states what is and what is not allowed in a system during normal operation; it consists of a set of rules that could be expressed in formal, semi-formal or very informal language. In many contexts, a system can be considered secure and trustworthy if the policy enforced by its security administrator is trustworthy too; from this standpoint it is possible to evaluate the system security by evaluating its policy. In this paper we present a policy-based methodology to formalize and compare policies, and a Security Metric to evaluate the security level that a system is able to grant. All the steps of the methodology will be illustrated with an operative approach, by directly applying it to a real case study: the semi-automated Cross Certification among Public Key Infrastructures.

Fault trees are a well known mean for the evaluation of dependability of complex systems. Many extensions have been proposed to the original formalism in order to enhance the advantages of fault tree analysis for the design and assessment of systems. In this paper we propose an extension, repairable fault trees, which allows the designer to evaluate the effects of different repair policies on a repairable system: this extended formalism has been integrated in a multi-formalism multi-solution framework, and it is supported by a solution technique which transparently exploits generalized stochastic Petri nets (GSPN)for modelling the repairing process. The modelling technique and the solution process are illustrated through an example.

The DrawNet++ project addresses the compositional construction of dependability models. Its main goals are to provide: a) a GUI to any graph-based formalism; b) a support to the design process of dependability models, according to concepts inspired by object orientation (OO); c) a user friendly front-end for different classes of analysis/simulation tools.

Abstract A system supporting video on demand is modeled in the process calculus CCS (Calculus of Communicating Systems), while some properties are expressed in a temporal logic and verified by means of the model checkers of the North Carolina Concurrency Workbench. This application was chosen as a case study to evaluate the usefulness of a methodology, by means of which a property is checked on reduced models obtained issuing abstractions of the system on the basis of the formula. Experimental results are shown and discussed. Copyright © 2001 John Wiley & Sons, Ltd.

CSP and Petri Nets are powerful formalisms for the specification and the analysis of concurrent systems. We present an approach to their integration to take advantage of both formalisms. In particular the GSPN class is used to address dependability and real-time aspects. In this paper an algorithmic transformation from a trace-based specification of a concurrent system to a Petri Net model is described. Causal dependencies between behaviours of the system components are introduced in the net model through the definition of external assumptions. The steps of the integration are illustrated by applying them to an unmanned transportation problem.