1,721,041 research outputs found
ROS/Gazebo-Based Simulation of Quadcopter Aircrafts
The main purpose of this work is to present a tutorial description on how to design and develop an observer, which is capable of estimating the position and the orientation of a drone commanded by a controller, whose shape and structure are unknown. Starting from Newton's and Euler's laws, a mathematical model describing the dynamics of a quadcopter has first been obtained. By linearizing this model it is possible to implement a Luenberger observer and validate it with simulations in a Linux environment, thanks to the use of the Ardupilot controller and the Gazebo simulator. Finally, starting from the results obtained from the simulation, it is possible to evaluate the error made in the estimation by observer and reconstruct the trajectory traveled by the drone during the simulation
Convergence Analysis of Extended Kalman Filter for Sensorless Control of Induction Motor
This paper deals with convergence analysis of the extended Kalman filters (EKFs) for sensorless motion control systems with induction motor (IM). An EKF is tuned according to a six-order discrete-time model of the IM, affected by system and measurement noises, obtained by applying a first-order Euler discretization to a six-order continuous-time model. Some properties of the discrete-time model have been explored. Among these properties, the observability property is relevant, which leads to conditions that can be directly linked with the working conditions of the machine. Starting from these properties, the convergence of the stochastic state estimation process, in mean square sense, has been shown. The convergence is also explored with reference to the difference between the samples of the state of the continuous-time model and that estimated by the EKF. The results theoretically achieved have been also validated by means of experimental tests carried out on an IM prototype
Distributed misbehavior monitors for socially organized autonomous systems
In systems in which many heterogeneous agents operate autonomously, with competing goals and without a centralized planner or global information repository, safety and performance can only be guaranteed by "social" rules imposed on the behavior of individual agents. Social laws are structured in a way that they can be verified just by using local information made available to an agent by a small number of its neighbors. Automobile mobility with traffic rules and logistics robots in warehouses are canonical examples of such "regulated autonomy", but many other fairly-competing autonomous systems are to be expected shortly. In these systems, detecting whether an agent is not abiding by the rules is crucial for raising an alert and taking appropriate countermeasures. However, the limited visibility due to the local nature of the information makes the problem of misbehavior detection hard for any single agent, and only an exchange of information between agents can provide sufficient clues to arrive at a decision. This paper attacks the misbehavior detection problem for a class of socially organized autonomous systems, where the behavior of agents depends on the presence or absence of other neighbors. We propose a solution involving a "local monitor", which runs on each agent and includes a hybrid observer and a set-valued consensus node. Based on whatever visibility is available, it reconstructs a set-valued occupancy estimate of nearby regions and combines it with communicating neighbors to reach a shared view and a mismatch discovery. We provide a formal framework for describing social rules that unify many different applications and a tool to generate code automatically for local monitors. The technique is demonstrated in various systems, including self-driving cars, autonomous forklifts, and distributed power plants
Co-simulation and Formal Verification of Co-operative Drone Control With Logic-Based Specifications
Unmanned aerial vehicle (UAV) co-operative systems are complex cyber-physical systems that integrate a high-level control algorithm with pre-existing closed implementations of lower-level vehicle kinematics. In model-driven development, simulation is one of the techniques that are usually applied, together with testing, in the analysis of system behaviours. This work proposes a method and tools to validate the design of UAV co-operative systems based on co-simulation and formal verification. The method uses the Prototype Verification System, an interactive theorem prover based on a higher-order logic language, and the Functional Mock-up Interface, a widely accepted standard for co-simulation. In this paper, results on the co-simulation and proofs of safety requirements of a representative co-ordination algorithm are shown and discussed in a scenario where quadcopters are deployed and perform space-coverage operations
Erle-copter Simulation using ROS and Gazebo
The recent decrease in the price as well as size of semi-conductor logic and due to significant advancements in technologies such as microcontrollers, motors and sensors, the application of quadcopters in several fields has been achieved. However, testing of quadcopter prototypes still has a risk of damage due to faults and unexpected behavior. Hence, a method of testing of quadcopters in simulation mimicking the actual conditions of the real environment in an actual hardware test has been proposed. For this purpose, Gazebo simulator integrated with ROS has been chosen for the simulation of the path of the quadcopter. Moreover, the software Matlab/Simulink has been interfaced with Gazebo in order for the simulation of the quadcopter to be achieved
Integrated Simulation and Formal Verification of a Simple Autonomous Vehicle
This paper presents a proof-of-concept application of an approach to system development based on the integration of formal verification and co-simulation. A simple autonomous vehicle has the task of reaching an assigned straight path and then follow it, and it can be controlled by varying its turning speed. The correctness of the proposed control law has been formalized and verified by interactive theorem proving with the Prototype Verification System. Concurrently, the system has been co-simulated using the Prototype Verification System and the MathWorks Simulink tool: The vehicle kinematics have been simulated in Simulink, whereas the controller has been modeled in the logic language of the Prototype Verification System and simulated with the interpreter for the same language available in the theorem proving environment. With this approach, co-simulation and formal verification corroborate each other, thus strengthening developers' confidence in their analysis
Low-cost underwater navigation systems by multi-pressure measurements and AHRS data
This paper deals with accurate navigation for underwater remotely operated vehicles. A feasibility study for a multi-pressure device to be mounted on an ROV is presented. The device can provide accurate estimates of a ROV orientation and angular speed. It is based on the well-known total pressure principle, also used in a Pitot tube, and allows reconstruction of static and dynamic pressures, which in turn provide good estimates of the ROV's orientation and rotational speed, respectively. An appealing feature of the proposed device is its ability to provide accurate estimates even for low-speed movements
Block-Based Models and Theorem Proving in Model-Based Development
This paper presents a methodology to integrate computer-assisted theorem proving into a standard workflow for model-based development that uses a block-based language as a modeling and simulation tool. The theorem prover provides confidence in the results of the analysis as it guides the developers towards a correct formalization of the system under developmen
Online Estimation of the Mechanical Parameters of an Induction Machine Using Speed Loop characteristics and Recursive Least Square Technique
This paper presents a novel approach for estimation of mechanical parameters, inertia and friction coefficient of an Induction Machine (IM) using speed loop characteristics and Recursive Least Square (RLS) estimator. Using the 5th order dynamic equation for Induction Machine and the forgetting factor based RLS algorithm the technique herein proposed employs the speed of the machine and the torque as the inputs for the estimator. Results obtained compares the estimated parameters with the actual parameters under multiple step varying and exponentially varying scenarios. Upon analyzing the results, the validity and the effectiveness of the proposed identification technique is confirme
- …
