ABSTRACT. The presence of software is pervasive in the society, and, due to its impact on our routines, the concern about its quality and reliability is a matter of utmost importance, especially when it comes to critical systems. Although software testing is a crucial step in software production, it is typically associated with some risks and elevated costs, particularly, when carried out manually. Model-based testing (MBT) tools is a technique that is capable of changing this scenario, enabling automatic test design and execution. However, assessing the correctness of these tools, which are also software developed by humans, is a valid concern too. To alleviate this concern, formal testing approaches are proposed, encompassing a well-defined conformance relation, along with test generation and execution strategies. Moreover, it is typically expected a proof of the soundness of the proposed approach. Unfortunately, many of the devised conformance relations are only theoretically defined, or are associated with disconnected implementations, that is, with no rigorous guarantees that the proposed theory is implemented correctly. Here, we show how an industrial-strength interactive theorem prover (Rocq) can be used to simultaneously formalise and provide a correct mechanisation of conformance testing theories; bridging the gap between theory and practice.

ABSTRACT. The integration of Information and Communication Technologies (ICT) has become essential to enhancing urban infrastructure and addressing challenges in modern cities, particularly in urban mobility. Bus Rapid Transit (BRT) systems are crucial for enhancing mobility, but they require robust monitoring to ensure safety and service quality, particularly at high-traffic stations. This paper presents a hierarchical availability model for monitoring systems in BRT stations, combining Reliability Block Diagrams (RBDs) to represent the system structure and Continuous-Time Markov Chains (CTMCs) to model the dynamic behavior of Edge Computing components. The proposed approach supports the evaluation of system availability and informs decision-making in the design and planning of smart urban infrastructure. A case study demonstrates the model's applicability in a realistic IoT-enabled BRT environment, highlighting its effectiveness in estimating availability metrics and improving service resilience. Evaluation results indicated a baseline system availability of 99.70%, translating to nearly 26 hours of annual downtime. Sensitivity analysis revealed the Edge computing unit as the most critical component, and implementing warm standby redundancy for this unit substantially improved system availability, reducing annual downtime by up to 76% in evaluated scenarios.

ABSTRACT. Workflows coordinate tasks across departments or organisations, where correct execution depends not only on control dependencies but also on the availability of shared resources. This paper presents ReAct, a resource-aware active object language for workflow modelling. In ReAct, method declarations serve as contracts: they specify alternative resource profiles in their signatures, giving methods multiple execution options when resources are limited. Methods can be invoked only once their dependency conditions are satisfied; at activation, a feasible resource profile is then selected and allocated. We encode the language in Maude and show how workflows can be executed, simulated, and verified against their declared dependencies and resource requirements.