Engineering topics

Mavridou, Anastasia

Publications and source records attributed to Mavridou, Anastasia.

5 records

NASA NTRS2020

Formal Requirements Elicitation with FRET

FRET is a tool for writing, understanding, formalizing and analyzing requirements. Users write requirements in an intuitive, restricted natural language, called FRETISH, with precise, unambiguous meaning. For a FRETISH requirement, FRET: 1) produces natural language and diagrammatic explanations of its exact meaning, 2) formalizes the requirement in logics, and 3) supports interactive simulation of produced logic formulas to ensure that they capture user intentions. FRET connects to analysis tools by facilitating the mapping between requirements and models/code, and by generating verification code. FRET is available open source at https://github.com/NASA-SW-VnV/fret; a video can be accessed at : https://tinyurl.com/fretForREFSQ.

Giannakopoulou, Dimitra↗

NASA NTRS2020

Bridging the Gap Between Requirements and Simulink Model Analysis

Formal verification and simulation are powerful tools for the verification of requirements against complex systems. Requirements are developed in early stages of the software lifecycle and are typically expressed in natural language. There is a gap between such requirements and their software implementations.We present a framework that bridges this gap by supporting a tight integration and feedback loop between high-level requirements and their analysis against software artifacts. Our framework implements an analysis portal within the fret requirements elicitation tool, thus forming an end-to-end, open-source environment where requirements are written in an intuitive, structured natural language, and are verified automatically against Simulink models.

Mavridou, Anastasia↗

NASA NTRS2020

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

Formal verfication and simulation are powerful tools to validate requirements against complex systems. [Problem] Requirements are developed in early stages of the software lifecycle and are typically written in ambiguous natural language. There is a gap between such requirements and formal notations that can be used by verification tools, and lack of support for proper association of requirements with software artifacts for verification. [Principal idea] We propose to write requirements in an intuitive, structured natural language with formal semantics, and to support formalization and model/code verification as a smooth, well-integrated process. [Contribution] We have developed an end-to-end, open source requirements analysis framework that checks Simulink models against requirements written in structured natural language. Our framework is built in the Formal Requirements Elicitation Tool (fret); we use fret's requirements language named fretish, and formalization of fretish requirements in temporal logics. Our proposed framework contributes the following features: 1) automatic extraction of Simulink model information and association of fretish requirements with target model signals and components; 2) translation of temporal logic formulas into synchronous dataflow cocospec specifications as well as Simulink monitors, to be used by verification tools; we establish correctness of our translation through extensive automated testing; 3) interpretation of counterexamples produced by verification tools back at requirements level. These features support a tight integration and feedback loop between high level requirements and their analysis. We demonstrate our approach on a major case study: the Ten Lockheed Martin Cyber-Physical, aerospace-inspired challenge problems.

Mavridou, Anastasia↗

NASA NTRS2019

Formalizing and Analyzing Requirements with FRET

Formal verification and simulation are powerful tools to validate requirements against complex systems. Requirements are developed in early stages of the software lifecycle and are typically written in ambiguous natural language. There is a gap between such requirements and formal notations that can be used by verification tools, and lack of support for proper association of requirements with software artifacts for verification. We propose to write requirements in an intuitive, structured natural language with formal semantics, and to support formalization and model/code verification as a smooth, well-integrated process. To this end, we have developed an end-to-end, open source requirements analysis framework that checks Simulink models against requirements written structured natural language.

Mavridou, Anastasia↗

NASA NTRS2019

Integrating Realizability Checking in FRET

Realizability (alternatively referred to as relative consistency or implementability) - checking whether a specification can be implemented by an open system - has been the subject of extensive study. Realizability can be viewed as a stronger analysis method when compared to consistency checking in that it does not only check whether the system works in some environment, but instead whether the system works in all environments. In this report, we experiment and build on the approach presented by Gacek et al. that supports checking realizability of contracts involving infinite theories using SMT solvers. In particular, we 1) extend the Formal Requirements Elicitation Tool (FRET) to support generation of Lustre contracts that can be checked for realizability with the JKind k-induction and fix point generation engines; 2) study a compositional way for checking realizability based on the notion of connected components; and 3) test our approach and the capabilities of the JKind realizability engines on a large subset of the Lockheed Martin Cyber Physical System Challenge Problems.

Kooi, David↗