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 future-time and past-time temporal logic, 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 veri cation code. fret is available open source at https://github.com/NASA-SW-VnV/fret; a video can be accessed at: https://tinyurl.com/fretForREFSQ.
Novelty. fret incorporates ideas from several existing approaches to requirements engineering. The structure
of fretish requirements includes features from temporal logic, the Speci cation Pattern System (SPS) [
This section describes a user's end-to-end interaction with fret through an example from the publicly-available
Lockheed Martin Cyber Physical Systems (LMCPS) challenge [
Requirements Elicitation. Figure 2 illustrates fret's requirements elicitation interface. fretish requirement [AP-002a]:\in roll hold mode RollAutopilot shall always satisfy autopilot engaged & no other lateral mode" expresses the natural language description included in the \Rationale and Comments" eld. i.e., that the autopilot should be engaged and no other lateral mode should be active when the Roll Autopilot is in roll hold mode. The interface window consists of the editor, on the left, and a help tab on the right (gray background). The fretish grammar, displayed as \railroad diagrams", is accessible from this view by clicking on the question mark.
A fretish requirement description is automatically parsed into six sequential elds, with the fret editor dynamically coloring the text corresponding to the elds as the requirement is typed in (Figure 2): scope, condition, component , shall , timing , and response. Help and examples on each speci c eld can be displayed in the help tab by clicking on the corresponding eld bubble. The mandatory component eld speci es the component that the requirement applies to (RollAutopilot). The shall keyword states that the component behavior must conform to the requirement. The response eld currently is of the form satisfy R, where R is a non-temporal Boolean-valued expression.
Field scope (optional) states that the requirement is only relevant in speci c scopes of the system behavior, for example when the system is \in roll hold mode". The Boolean expression eld condition (optional) states that, within the speci ed mode, the requirement becomes relevant only from the point where the condition becomes true. When, as in our example, condition is omitted, there is no such restriction. Field timing (optional) speci es at which points the response must occur, for example \always", meaning at all points where the system is \in roll hold mode". Default timing is eventually .
By clicking semantics, the help tab displays various explanations of the requirement, as well as temporal formulas. The diagram of Figure 2 illustrates that the requirement is only relevant within the grayed box M (M represents intervals where the Autopilot is in \roll hold" mode). The green band states that \autopilot engaged & no other lateral mode" is required to hold at all time points within the gray box.
Requirements Visualization. Getting a requirement with temporal relationships right is a tricky and
subtle task. Errors and misunderstandings might creep into the formulation, resulting in a requirement that
does not correctly re ect the temporal interdependencies of the involved signals. Based upon the graphical
signal representation commonly used in digital electronics, we developed an interactive requirements visualizer
in fret, available by clicking simulate in the semantics view of the help tab (see Figure 2). Given a fret
requirement, it shows temporal traces of each of the signals (variables) involved as well as the valuation of the
requirement for each point in time (see Figure 4). The user can interactively modify the input signals; the
valuation of the requirement is updated automatically and thus makes it possible for the user to visually inspect
the temporal behavior of the requirement. The valuation is computed based on the construction of a nite state
machine from the input trace, which is then veri ed against the metric linear temporal logic (LTL) formalization
of the requirement, using the model checker NuSMV [
Requirements Analysis. fret's main purpose is to facilitate the
elicitation of unambiguous requirements. For analysis, it allows users to
export requirements in formats that can be digested by external analysis
tools. fret currently connects to the CoCoSim tool [3] for analysis of
Simulink models, and through CoCoSim to the Kind2 [
To analyze requirements against an implementation as model or code, one needs to associate the requirement variables, which are at a high level, with variables in the model or code (signals in the case of Simulink).
Moreover, fret needs to generate veri cation code that can be understood by the target analysis tool. To connect with CoCoSim, fret transforms requirements into CoCoSpec code. In this process, fret supports the import of Simulink model information provided by CoCoSim, and association of high-level requirements with target model signals and components (see Figure 5).
fret is implemented mainly in JavaScript as an Electron JS app. Electron JS2 is a framework for creating
desktop-suite applications by using web development programming languages. Electron JS uses two main
technologies: the Node.js runtime and the Chromium web browser. Its le system provided through the Node.js
API is compatible with Linux, Mac OS, and Windows. fret's interactive interface was developed with the
React JavaScript library3. fret uses PouchDB4as an in-browser database that also runs in Node.js. fret's
architecture is illustrated in Figure 6. This section reviews the main modules in the architecture.
O ine Formalization. Formalization of fretish requirements is performed by the formalizer component,
which is described in detail in [
2https://electronjs.org/ 3 https://reactjs.org/
English language explanations and diagrams, which are all saved in a cache. Note that all these artefacts are templates that contain variables. These variables get instantiated by fret to capture the details of speci c requirements, as will be described later.
formalization verifier is a modular, extensible framework, which provides assurance that formulas generated by the formalizer capture the intended semantics. It implements 1) a module that generates traces, i.e., example executions over which to interpret formulas; 2) a module that, given a trace and a template key, generates an expected value of true or false based on the semantics of the fretish language, 3) a module which interprets formulas over traces and compares the outcome to expected values, and 4) a module that compares future and past-time formulas generated for the same template key, for equivalence.
s y e k te a l p m te e s l a F / e u r T
trace generator oracle formalizer formula diagram explanation
cache formalization verifier seemvaalunatitcosr eqcuhiveackleenrce fretish parser editor/elicitor LTL formulas visualizer simulator template key requirement elds
analysis portal architectural data requirements-model
mapper formula translator
veri cation code + traceability data instantiator formalized requirement (explanation + diagram + formulas) Requirements Elicitation. The bulk of the work in formalizing fretish requirements is performed o ine and cached. When users write a requirement, the parser identi es the corresponding template key, and the values of the requirement elds, which instantiate the template key. The instantiator uses the template key to fetch correct artefacts from the cache, and uses the requirement elds to appropriately instantiate them. The produced LTL formulas can be explored interactively through the simulator.
Analysis Portal. This component connects fret with analysis tools. The user needs to de ne mappings between fretish variables and model variables, as well as additional information such as variable types, which is not relevant at a high level. Module requirements-model mapper supports this process and stores the provided information in a database. It is also able to import architectural data about model components and signals, when available, to facilitate this task. Module formula translator currently uses information from the mapper, and the past-time LTL formalization of a requirement, to generate CoCoSpec code, as well as traceability data. The latter is used to report analysis results in the context of fretish requirements. This component could also be used in the context of other tools, and is described in detail in [14]. 4
As mentioned, we have successfully applied fret to the LMCPS industrial case study; a detailed evaluation
is provided in [
More generally, now that fret has its basic features established, we are focusing on improving the interaction with users both in editing and correcting requirements. Similarly, we are working on additional analysis tools/algorithms to integrate with fret; for example, we have been developing support for checking requirements realizability. In general, given fret's open source status, we hope to obtain feedback and contributions from the wider research community. For example, we expect that as the tool gets used in various domains, fretish could be extended or customized accordingly. Moreover, researchers could connect fret to issue and project tracking systems, requirements management systems, assurance case environments, as well as additional analysis tools. Acknowledgements. We thank David Bushnell and Tanja de Jong for working on early prototypes of fret. This work was funded by the NASA ARMD System-Wide Safety Project. [3] CoCo-team: CoCoSim { automated analysis framework for Simulink. the version used in this paper is a closed source version of the tool at NASA Ames that is based on the open source version. https://github.com/ coco-team/cocoSim2 use
Software 29(2), 17{18