Title: Formal Methods Seminar: A Graphics Library for Rapid Prototyping Interactive Cockpit Displays
Speaker: Paolo Masci, Senior Research Scientist, NIA
When: Friday, February 15, 2019
Location: NASA/LaRC, B1230-R264A
Contact: Cesar Munoz, NASA/LaRC
Abstract: This talk introduces a preliminary version of an open-source framework for rapid prototyping and analysis of interactive cockpit displays. A library of widgets is provided that captures the characteristics and functionalities of common interactive elements in real cockpit displays, such as compass, altitude/airspeed tapes, and interactive maps. The functional logic driving the behavior of the widgets is separated from event handling and visual rendering, facilitating re-use of prototype front-ends for functional specifications written in different languages, including executable formal models and software implementations. Simulation tools are also provided for comparative analysis of simulation runs, e.g., playback/logging of interactive simulations, and side-to-side visualization of parallel simulation runs executed in lock-step. This framework aims to facilitate the use of formal methods within a multi-disciplinary team of developers, where a constructive dialogue needs to be established between formal methods experts, pilots, human factors specialists, and software engineers. An example application is presented based on a cockpit system developed at NASA.
Biography: Paolo Masci, is a Senior Research Scientist with the Formal Methods Group at NIA. Prior to joining NIA, Paolo carried out his research in different institutions, including INESC-TEC and Universidade do Minho (Portugal), Queen Mary University of London (UK), Italian National Research Council (Italy), and University of Pisa (Italy). From 2012 to 2018, he was visiting researcher at the US Food and Drug Administration (FDA), and his main research focus was on tools and methods for early identification of software anomalies in medical devices. At NIA, Paolo conducts research on theorem proving technology for verification of safety-critical aerospace applications. His research interest include verification of human-machine interfaces, co-simulation technologies, and rapid prototyping.