0000000000614821
AUTHOR
Cinzia Bernardeschi
showing 5 related works from this author
Co-simulation and Formal Verification of Co-operative Drone Control With Logic-Based Specifications
2021
Abstract 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-…
Demo: Co-simulation of UAVs with INTO-CPS and PVSio-web
2018
This demo shows our ongoing work on the co-simulation of co-operative Unmanned Aerial Vehicles (UAVs). The work is based on the INTO-CPS co-simulation engine, which adopts the widely accepted Functional Mockup Interface (FMI) standard for co-simulation, and the PVSioweb prototyping tool, that extends a system simulator based on the PVS logic language with a web-based graphical interface. Simple scenarios of Quadcopters with assigned different tasks, such as rendez-vous and space coverage, are shown. We assumed a linearized dynamic model for Quadcopters formalized in OpenModelica, and a linearized set of equations for the flight control module written in C language. The co-ordination algorit…
Co-simulation of bio-inspired multi-agent algorithms
2020
This paper reports on the co-simulation of a team of robots deployed in an exploration task, coordinated by a bio-inspired exploration algorithm. The co-simulation integrates the high-level exploration algorithm with detailed implementations of the robot controllers and kinematic models. Co-simulation results are used to find and correct mismatches between submodels.
ROS/Gazebo Based Simulation of Co-operative UAVs
2019
UAVs can be assigned different tasks such as e.g., rendez-vous and space coverage, which require processing and communication capabilities. This work extends the architecture ROS/Gazebo with the possibility of simulation of co-operative UAVs. We assume UAV with the underlying attitude controller based on the open-source Ardupilot software. The integration of the co-ordination algorithm in Gazebo is implemented with software modules extending Ardupilot with the capability of sending/receiving messages to/from drones, and executing the co-ordination protocol. As far as it concerns the simulation environment, we have extended the world in Gazebo to hold more than one drone and to open a specif…
Block-Based Models and Theorem Proving in Model-Based Development
2021
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 development.