CPSRC Seminar: Bridging the Gap Between Requirements and Model Analysis: Evaluation on Ten Cyber-Physical Challenge Problems

Speaker Name: 
Anastasia Mavridou
Speaker Title: 
Computer Scientist
Speaker Organization: 
NASA Ames Research Center
Start Time: 
Thursday, May 2, 2019 - 1:30pm
End Time: 
Thursday, May 2, 2019 - 3:00pm
Location: 
E2 599
Organizer: 
Ricardo Sanfelice

 

Abstract

 

We present a framework for introducing high-level requirement  specifications in the automated analysis of dataflow models.  By integrating the Formal Requirements Elicitation Tool (FRET) with  the CoCoSim analyzer, our framework enables the analysis of hierarchical  Simulink models against requirements written in a restricted English language. More precisely, we support: automatic extraction of Simulink model information and association of high-level requirements with target model signals and components; translation of temporal logic formulas into synchronous  dataflow specifications as well as Simulink monitors; and interpretation of counterexamples produced by the analysis both at the requirement and model levels. For the analysis, we use the Kind2, Zustre, and Simulink Design Verifier (SLDV) tools. The features provided by our framework are generic and can be used to integrate other requirements elicitation and Simulink/Lustre analysis tools. We report on lessons learned  from the application of our approach to the Lockheed Martin Cyber-Physical, aerospace-inspired challenge problems.

 

Bio

 

Anastasia Mavridou is a Computer Scientist at the Robust Software Engineering group at NASA Ames. Previously, she was a PostDoctoral Researcher at the Institute for Software Integrated Systems at Vanderbilt University. She received her PhD in 2016 from Ecole Polytechnique Fédérale de Lausanne (EPFL), Switzerland. Her research interests revolve around formal modeling and analysis of systems with a focus on correct-by-construction techniques.