showing 5 related works from this author
Integrated Simulation and Formal Verification of a Simple Autonomous Vehicle
2018
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 t…
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.
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.