GRAPHICAL ANIMATION OF DAIDALUS FORMAL METHODS
Piergiuseppe Mallozzi, University of Pisa, Italy
August 21, 2015, 1:00 pm, NASA Langley, Bldg 1220, Rm 110
Abstract:
This talk presents a graphical animation of the functional specifications of the Detect and Avoid Alerting Logic for Unmanned Systems (DAIDALUS). The graphical animation integrates an interactive graphical front-end with formal models. The graphical front-end is implemented using WorldWind, an open-source virtual globe simulation library developed at NASA. The formal back-end relies on formal models written in the Program Verification System (PVS) and evaluated within PVSio, the animation environment of PVS. The front-end and the back-end are integrated using PVSio-web, a toolk that enables co-simulation and seamless exchange of messages and data between PVSio and other simulation environments.
Bio:
Mr. Mallozzi is a MSc student from the University of Pisa, Italy