Anastasia Mavridou works as a researcher at KBR/NASA Ames Research Center, Mountain View, California, USA. She is a member of the Robust Software Engineering Group. Her research interests focus on the use of formal methods for the description and verification of critical systems. In recent years she has been working in the area of requirements engineering, specifically in the open source tool FRET at NASA Ames Research Center. For her work on FRET she has been honored, together with the rest of the FRET team, with the NASA Group Achievement Award. Last year she co-chaired the NFM 2020 (NASA Formal Methods Symposium) conference and this year she is co-organizing FMICS 2021 (Formal Methods for Industrial Critical Systems). Anastasia Mavridou holds a Diploma in Electrical and Computer Engineering from the Aristotle University of Thessaloniki and a PhD from the Polytechnic University of Lausanne (EPFL), supervised by Professor Joseph Sifakis.
Capturing and Analyzing Requirements with NASA Ames’ FRET
Requirements engineering is a central step in the development of safety-critical systems. In practice, requirements are typically written in natural language, which is ambiguous and consequently not amenable to formal analysis. Since formal, mathematical notations are usually unintuitive, requirements in FRET are entered in a restricted natural language. For each requirement, FRET automatically produces temporal logic formulas and verification code that can be used by analysis tools at all phases of the software lifecycle. In this talk, we will demonstrate the process of writing, explaining, formalizing, and analyzing aerospace requirements with the FRET tool. FRET is developed at NASA Ames.