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.

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.

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.

This paper describes use of model checking to verify synchronisation properties of an industrial welding system consisting of a cobot arm and an external turntable. The robots must move synchronously, but sometimes get out of synchronisation, giving rise to unsatisfactory weld qualities in problem areas, such as around corners. These mistakes are costly, since time is lost both in the robotic welding and in manual repairs needed to improve the weld. Verification of the synchronisation properties has shown that they are fulfilled as long as assumptions of correctness made about parts outside the scope of the model hold, indicating limitations in the hardware. These results have indicated the source of the problem, and motivated a re-calibration of the real-life system. This has drastically improved the welding results, and is a demonstration of how formal methods can be useful in an industrial setting.

The ongoing efforts to deploy safety-critical autonomous robots that operate in semi-structured, dynamic, and uncertain environments, reinforce the importance of supplementing traditional risk-management activities, input-based testing, and quality assurance procedures, with formal verification methods. With this approach, one may guarantee safe behavior in all relevant scenarios. In this paper, we propose a safety assurance framework enabling the integrated use of formal verification at all stages of the engineering life-cycle, beginning at the concept study, design, development, deployment, and operation. Along the way, a real use case from the agricultural industry, namely robotic ultra-violet (UVC) plant treatment, is used to demonstrate the proposed methodology. In particular, the transfer of offline model-checking artifacts to Runtime Verification elucidates how safety requirements can be conceptualized and subsequently translated into online monitors that are integrated seamlessly with the robot’s control system. Our study elaborates on the modeling and verification process, and on the accompanying monitoring tool chain that facilitates the integration in ROS2 applications.

Continued adoption of agricultural robots postulates the farmer's trust in the reliability, robustness and safety of the new technology. This motivates our work on safety assurance of agricultural robots, particularly their ability to detect, track and avoid obstacles and humans. This paper considers a probabilistic modelling and risk analysis framework for use in the early development phases. Starting off with hazard identification and a risk assessment matrix, the behaviour of the mobile robot platform, sensor and perception system, and any humans present are captured using three state machines. An auto-generated probabilistic model is then solved and analysed using the probabilistic model checker PRISM. The result provides unique insight into fundamental development and engineering aspects by quantifying the effect of the risk mitigation actions and risk reduction associated with distinct design concepts. These include implications of adopting a higher performance and more expensive Object Detection System or opting for a more elaborate warning system to increase human awareness. Although this paper mainly focuses on the initial concept-development phase, the proposed safety-assurance framework can also be used during implementation, and subsequent deployment and operation phases.

This study identifies the keys for successful collaboration between the communities of academia and practice in the field of automation and control. The findings are based on the analysis of 85 different collaborations reported in a survey of the international control community conducted by the Industry and Education Committees at IFAC. Addressing a joint problem, understanding and respecting each other, frequent communication, and adequate funding are among the top attributes of successful collaboration. A complete list of the top 10 keys for success is provided in the conclusion section.

As a general trend in industrial robotics, an increasing number of safety functions are being developed or re-engineered to be handled in software rather than by physical hardware such as safety relays or interlock circuits. This trend reinforces the importance of supplementing traditional, input-based testing and quality procedures which are widely used in industry today, with formal verification and model-checking methods. To this end, this paper focuses on a representative safety-critical system in an ABB industrial paint robot, namely the High-Voltage electrostatic Control system (HVC). The practical convergence of the high-voltage produced by the HVC, essential for safe operation, is formally verified using a novel and general co-verification framework where hardware and software models are related via platform mappings. This approach enables the pragmatic combination of highly diverse and specialised tools. The paper's main contribution includes details on how hardware abstraction and verification results can be transferred between tools in order to verify system-level safety properties. It is noteworthy that the HVC application considered in this paper has a rather generic form of a feedback controller. Hence, the co-verification framework and experiences reported here are also highly relevant for any cyber-physical system tracking a setpoint reference.

Due to the risk of discharge sparks and ignition, there are strict rules concerning the safety of high voltage electrostatic systems used in industrial painting robots. In order to assure that the system fulfils its safety requirements, formal verification is an important tool to supplement traditional testing and quality assurance procedures. The work in this paper presents formal verification of the most important safety functions of a high voltage controller. The controller has been modelled as a finite state machine, which was formally verified using two different model checking software tools; Simulink Design Verifier and RoboTool. Five safety critical properties were specified and formally verified using the two tools. Simulink was chosen as a low-threshold entry point since MathWorks products are well known to most practitioners. RoboTool serves as a software tool targeted towards model checking, thus providing more advanced options for the more experienced user. The comparative study and results show that all properties were successfully verified. The verification times in both tools were in the order of a few minutes, which was within the acceptable time limit for this particular application.

Due to the immutable nature of distributed ledger technology such as blockchain, it is of utter importance that a smart contract works as intended before employment outside test network. This is since any bugs or errors will become permanent once published to the live network, and could lead to substantial economic losses; as manifested in the infamous DAO smart contract exploit hack in 2016. In order to avoid this, formal verification methods can be used to ensure that the contract behaves according to given specifications. This paper presents a survey of the state of the art of formal verification of smart contracts. Being a relatively new research area, a standard or best practice for formal verification of smart contracts has not yet been established. Thus, several different methods and approaches have been used to perform the formal verification. The survey presented in this paper shows that some variant of model checking or theorem proving methodology seems to be most successful. However, as of today, formal verification is only successful on simple contracts, and does not support more advanced smart contract syntax.

Given the total power demand, Pd, current practice of equal load sharing in the process industry is to distribute the load among power supply units and machines (e.g., diesel/gas/wind turbines) in proportion to the maximum power, i.e., P i = P max i /Σ i P d , where P max i denotes the maximum power of the i th unit. However, the efficiency of power supply units, vary in time and are highly individual, even in the case of units from same brand and model. Thus, by considering and utilizing these individual differences, it is possible to share the load in a more fuel/cost/energy optimal manner. To capture this potential, the work presented in this paper proposes an optimization and learning-based approach for sharing the load among a set of heterogeneous power supply units. The main contributions of this paper include formulation of the overall energy management system algorithm, including power grid connection and Energy Storage System (ESS), as a Mixed Integer Non-Linear Program (MINLP), as well as algorithms for robust moving horizon estimation of efficiency curves and machine learning-based algorithms for classification of turbine state and prediction of future power demand needed for the predictive planning scheme. The soundness and performance of the proposed algorithms are verified using actual data from a power plant including gas turbines and power grid connection in combination with ESS.

Despite recent rapid advances and successful large-scale application of deep Convolutional Neural Networks (CNNs) using image, video, sound, text and time-series data, its adoption within the oil and gas industry in particular have been sparse. In this paper, we initially present an overview of opportunities for deep CNN methods within oil and gas industry, followed by details on a novel development where deep CNN have been used for state classification of autonomous gas sample taking procedure utilizing an industrial robot. The experimental results — using a deep CNN containing six layers — show accuracy levels exceeding 99 %. In addition, the advantages of using parallel computing with GPU is re-confirmed by showing a reduction factor of 43,8 for the training time required as compared with a CPU implementation. Finally, by analyzing the variations in the output probability distribution, it is shown that the deep CNN can also detect a number of undefined and therefore untrained anomalies. This is an extremely appealing property and serves as an illustrative example of how deep CNN algorithms can contribute towards safer and more robust operation in the industry.

In this paper we present an experimental study on real-time collision avoidance with potential fields that are based on 3D point cloud data and processed on the Graphics Processing Unit (GPU). The virtual forces from the potential fields serve two purposes. First, they are used for changing the reference trajectory. Second they are projected to and applied on torque control level for generating according nullspace behavior together with a Cartesian impedance main control loop. The GPU algorithm creates a map representation that is quickly accessible. In addition, outliers and the robot structure are efficiently removed from the data, and the resolution of the representation can be easily adjusted. Based on the 3D robot representation and the remaining 3D environment data, the virtual forces that are fed to the trajectory planning and torque controller are calculated. The algorithm is experimentally verified with a 7-Degree of Freedom (DoF) torque controlled KUKA/DLR Lightweight Robot for static and dynamic environmental conditions. To the authors knowledge, this is the first time that collision avoidance is demonstrated in real-time on a real robot using parallel GPU processing.

This paper presents adaptable methods for achieving fast collision detection using the GPU and Nvidia CUDA together with Octrees.Earlier related work have focused on serial methods, while this paper presents a parallel solution which shows that there is a great increase in time if the number of operations is large.Two different models of the environment and the industrial robot are presented, the first is Octrees at different resolutions, the second is a point cloud representation.The relative merits of the two different world model representations are shown.In particular, the experimental results show the potential of adapting the resolution of the robot and environment models to the task at hand.

Developing a reliable and intelligent robotic system which enables the remote operation of normally unmanned oil and gas facilities requires innovative and novel technical solutions. Our strategy for meeting these challenges is based on a step-wise approach involving development and validation of the technology in increasingly demanding settings. This starts with proof-of-concept demonstrations in our indoor test facility located in Oslo, Norway. Taking this one step further, robots and applications are further developed, tested and validated in a colocated outdoor test facility. This is normally an intermediate step before bringing demonstrators onto real oil and gas facilities. In this paper, this design philosophy is elaborated upon and illustrated using the development of a valve manipulation application as an example.

Deploying industrial robots in harsh outdoor environments require additional functionalities not currently provided. For instance, movement of standard industrial robots are pre-programmed to avoid collision. In dynamic and less structured environments, however, the need for online detection and avoidance of unmodelled objects arises. This paper focus on online obstacle detection using a laser sensor by proposing three different approaches, namely a CAD-based Expert System (ES) and two probabilistic methods based on a Hidden Markov Model (HMM) which requires observation based training. In addition, this paper contributes by providing a comparison between the CAD-based ES and the two versions of the HMM, one trained with real sensor data, and one where virtual sensor data has been extracted from the CAD-model and used during the training phase.

This paper presents a comparison of two approaches for detecting unknown obstacles inside the workspace of an industrial robot using a laser rangefinder for 2-D measurements. The two approaches are based on Expert System (ES) and Hidden Markov Model (HMM). The results presented in the paper demonstrate that both approaches are able to correctly detect and classify unknown objects. The ES is characterised by low computational requirements and an easy setup when relatively few known objects are to be included inside the workspace. HMMs are characterised by a higher flexibility and the ability to handle a larger amount of known objects inside the workspace. Another significant benefit of the HMM approach taken in this paper, in contrast to voice recognition, is the fact that the learnt parameters of the HMMs have physical meaningful geometrical interpretations.

The focus of this paper is our recent real-world demonstration using an industrial robot certified for running in explosive atmospheres (ATEX). The demonstration is run amidst live and running hydrocarbon processes and involves autonomous valve manipulation and thermal inspection operations. The valve manipulation operation involves sensor-based movements which implies that the robot trajectories have not been programmed a priori (off-line). In particular, an approach will be presented to sense and avoid over-tightening/loosening of the valve. To the best of our knowledge, this prototype is the first system that performs sensor-based close-contact operations in a real operational environment.