اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدTowards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management
263
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
The battery is a key component of autonomous robots. Its performance limits the robots safety and reliability. Unlike liquid-fuel, a battery, as a chemical device, exhibits complicated features, including (i) capacity fade over successive recharges and (ii) increasing discharge rate as the state of charge (SOC) goes down for a given power demand. Existing formal verification studies of autonomous robots, when considering energy constraints, formalise the energy component in a generic manner such that the battery features are overlooked. In this paper, we model an unmanned aerial vehicle (UAV) inspection mission on a wind farm and via probabilistic model checking in PRISM show (i) how the battery features may affect the verification results significantly in practical cases; and (ii) how the battery features, together with dynamic environments and battery safety strategies, jointly affect the verification results. Potential solutions to explicitly integrate battery prognostics and health management (PHM) with formal verification of autonomous robots are also discussed to motivate future work.
قيم البحث
اقرأ أيضاً
We aim to enable an autonomous robot to learn new skills from demo videos and use these newly learned skills to accomplish non-trivial high-level tasks. The goal of developing such autonomous robot involves knowledge representation, specification min
ing, and automated task planning. For knowledge representation, we use a graph-based spatial temporal logic (GSTL) to capture spatial and temporal information of related skills demonstrated by demo videos. We design a specification mining algorithm to generate a set of parametric GSTL formulas from demo videos by inductively constructing spatial terms and temporal formulas. The resulting parametric GSTL formulas from specification mining serve as a domain theory, which is used in automated task planning for autonomous robots. We propose an automatic task planning based on GSTL where a proposer is used to generate ordered actions, and a verifier is used to generate executable task plans. A table setting example is used throughout the paper to illustrate the main ideas.
Modularity is a central principle throughout the design process for cyber-physical systems. Modularity reduces complexity and increases reuse of behavior. In this paper we pose and answer the following question: how can we identify independent `modul
es within the structure of reactive control architectures? To this end, we propose a graph-structured control architecture we call a decision structure, and show how it generalises some reactive control architectures which are popular in Artificial Intelligence (AI) and robotics, specifically Teleo-Reactive programs (TRs), Decision Trees (DTs), Behavior Trees (BTs) and Generalised Behavior Trees ($k$-BTs). Inspired by the definition of a module in graph theory, we define modules in decision structures and show how each decision structure possesses a canonical decomposition into its modules. We can naturally characterise each of the BTs, $k$-BTs, DTs and TRs by properties of their module decomposition. This allows us to recognise which decision structures are equivalent to each of these architectures in quadratic time. Our proposed concept of modules extends to formal verification, under any verification scheme capable of verifying a decision structure. Namely, we prove that a modification to a module within a decision structure has no greater flow-on effects than a modification to an individual action within that structure. This enables verification on modules to be done locally and hierarchically, where structures can be verified and then repeatedly locally modified, with modules replaced by modules while preserving correctness. To illustrate the findings, we present an example of a solar-powered drone controlled by a decision structure. We use a Linear Temporal Logic-based verification scheme to verify the correctness of this structure, and then show how one can modify modules while preserving its correctness.
In this paper, we characterize the performance of and develop thermal management solutions for a DC motor-driven resonant actuator developed for flapping wing micro air vehicles. The actuator, a DC micro-gearmotor connected in parallel with a torsion
al spring, drives reciprocal wing motion. Compared to the gearmotor alone, this design increased torque and power density by 161.1% and 666.8%, respectively, while decreasing the drawn current by 25.8%. Characterization of the actuator, isolated from nonlinear aerodynamic loading, results in standard metrics directly comparable to other actuators. The micro-motor, selected for low weight considerations, operates at high power for limited duration due to thermal effects. To predict system performance, a lumped parameter thermal circuit model was developed. Critical model parameters for this micro-motor, two orders of magnitude smaller than those previously characterized, were identified experimentally. This included the effects of variable winding resistance, bushing friction, speed-dependent forced convection, and the addition of a heatsink. The model was then used to determine a safe operation envelope for the vehicle and to design a weight-optimal heatsink. This actuator design and thermal modeling approach could be applied more generally to improve the performance of any miniature mobile robot or device with motor-driven oscillating limbs or loads.
Ensuring that autonomous space robot control software behaves as it should is crucial, particularly as software failure in space often equates to mission failure and could potentially endanger nearby astronauts and costly equipment. To minimise missi
on failure caused by software errors, we can utilise a variety of tools and techniques to verify that the software behaves as intended. In particular, distinct nodes in a robotic system often require different verification techniques to ensure that they behave as expected. This paper introduces a method for integrating the various verification techniques that are applied to robotic software, via a First-Order Logic (FOL) specification that captures each nodes assumptions and guarantees. These FOL specifications are then used to guide the verification of the individual nodes, be it by testing or the use of a formal method. We also outline a way of measuring our confidence in the verification of the entire system in terms of the verification techniques used.
The Curiosity rover is one of the most complex systems successfully deployed in a planetary exploration mission to date. It was sent by NASA to explore the surface of Mars and to identify potential signs of life. Even though it has limited autonomy o
n-board, most of its decisions are made by the ground control team. This hinders the speed at which the Curiosity reacts to its environment, due to the communication delays between Earth and Mars. Depending on the orbital position of both planets, it can take 4--24 minutes for a message to be transmitted between Earth and Mars. If the Curiosity were controlled autonomously, it would be able to perform its activities much faster and more flexibly. However, one of the major barriers to increased use of autonomy in such scenarios is the lack of assurances that the autonomous behaviour will work as expected. In this paper, we use a Robot Operating System (ROS) model of the Curiosity that is simulated in Gazebo and add an autonomous agent that is responsible for high-level decision-making. Then, we use a mixture of formal and non-formal techniques to verify the distinct system components (ROS nodes). This use of heterogeneous verification techniques is essential to provide guarantees about the nodes at different abstraction levels, and allows us to bring together relevant verification evidence to provide overall assurance.
الأسئلة المقترحة
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
