This keynote presents CLEARSY’s journey from safety-critical railway automation to broader applications in autonomous mobility. Drawing from global deployments of automatic train systems, we show how railways function as large-scale robotic systems with embedded autonomy, localization, and fail-safe mechanisms. We then explore CLEARSY’s innovations in ground, aerial, and underwater autonomy, highlighting shared challenges in navigation, sensor fusion, and environment interaction. The role of advanced sensors, robust hardware, and formal modeling is emphasized across all domains. A core theme is the integration of safety, verification, and validation into robotics design—rooted in CLEARSY’s railway experience. The talk also addresses the transition from deterministic systems to complex, uncertain environments, proposing cross-domain methodologies for trustworthy autonomy. By bridging industry and research, CLEARSY supports the development of safe, deployable autonomous technologies. This keynote invites collaboration to ensure that the next generation of robotic systems is as safe as it is intelligent.
This paper presents the initial results from our structured literature review on applications of Formal Methods (FM) to Robotic Autonomous Systems (RAS). We describe our structured survey methodology; including database selection and associated search strings, search filters and collaborative review of identified papers. We categorise and enumerate the FM approaches and formalisms that have been used for specification and verification of RAS. We investigate FM in the context of sub-symbolic AI-enabled RAS and examine the evolution of how FM is used over time in this field. This work complements a pre-existing survey in this area and we examine how this research area has matured over time. Specifically, our survey demonstrates that some trends have persisted as observed in a previous survey. Additionally, it recognized new trends that were not considered previously including a noticeable increase in adopting Formal Synthesis approaches as well as Probabilistic Verification Techniques.
Autonomous robots deployed in shared human environments, such as agricultural settings, require rigorous safety assurance to meet both functional reliability and regulatory compliance. These systems must operate in dynamic, unstructured environments, interact safely with humans, and respond effectively to a wide range of potential hazards. This paper presents a verification workflow for the safety assurance of an autonomous agricultural robot, covering the entire development life-cycle, from concept study and design to runtime verification. The outlined methodology begins with a systematic hazard analysis and risk assessment to identify potential risks and derive corresponding safety requirements. A formal model of the safety controller is then developed to capture its behaviour and verify that the controller satisfies the specified safety properties with respect to these requirements. The proposed approach is demonstrated on a field robot operating in an agricultural setting. The results show that the methodology can be effectively used to verify safety-critical properties and facilitate the early identification of design issues, contributing to the development of safer robots and autonomous systems.
When teleoperating wheeled mobile manipulator robots using haptic devices, users usually use rate control for navigation and position control for manipulation. Manually switching between those two modes (for example, via a push button) while relying on visual feedback is often challenging, as using a single camera significantly reduces depth perception, making contact-based tasks difficult due to reduced spatial awareness and depth cues. Adding proximity sensors or auditory cues for distance detection requires processing more data, raising both the cognitive load and associated costs. On the other hand, typical automatic hybrid switching schemes employ restoring forces in navigation mode to assist the human operator. However, performing contact-based tasks in navigation mode deteriorates transparency due to interference between environmental and restoring forces while impairing fine-manipulation capabilities. Therefore, to overcome these challenges, we propose a new hybrid scheme that detects interaction with the environment via a force sensor to facilitate the automatic transition from navigation to manipulation mode. We use constrained task-space controllers to address obstacle avoidance directly in the control law and enable safe interaction. We conducted an ethically approved study involving nine humans to assess the proposed scheme and used task completion time (TCT) and NASA Task Load Index (TLX) to assess human operator workload. Paired t-tests indicate a reduction of 23.3% (. p = 0.0058) in TCT and mental demand by. 57.1% (. p = 0.0021), highlighting the advantages of the proposed semiautomatic switching scheme over the manual one.
This paper evaluates adaptive passive technologies for improving robotic locomotion in unstructured environments, focusing specifically on the Passively-Transformable Single-Part Wheel (PaTS-Wheel) and our novel variant, the “DogBone-Wheel.” We assessed these wheel designs in authentic woodland environments, measuring their energy efficiency, vibration profiles, and traversal capabilities in comparison to traditional wheels. Our findings demonstrate that the PaTS-Wheel achieved a superior obstacle-climbing ability (70 https://github.com/robert-stevenson-1/DogBone-Wheels .
