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 NA 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.