FRETish to LTL translation

[yingyingtran]

I'm on a team building an MBSE plug-in to make it easier to use model checkers on MBSE models, so the intended user is certainly unlikely to know how to write LTL. We are trying to enable understanding properties written in FRETish. I've been digging through the FRET source code, but can't figure out how FRETish is eventually translated to LTL for feeding into NuSMV. Better yet, is there some kind of API call that we can use for this translation?

[anmavrid]

Hi @yingyingtran,

Thanks for starting a new discussion! FRET's mission is to provide an intuitive platform for capturing precise requirements that are hard to specify directly in LTL.

Our formalization approach is detailed in the following paper: https://www.sciencedirect.com/science/article/abs/pii/S0950584921000707

In the code, we compute the formalizations through the compile method in app/parser/FretSemantics.js

Another feature that might be of interest to you is the following: we offer a way to invoke the requirement editor as a standalone tool in order to write a requirement in FRETish, check explanations/simulate and then export formalizations. Through this we can support easy integration with external tools. We explain how to use the standalone interface here: https://github.com/NASA-SW-VnV/fret/blob/master/fret-electron/docs/_media/user-interface/external/ext_tools.md

Is this helpful?

Thanks,
Anastasia

[yingyingtran]

Thank you for this thoughtful response! This provides excellent material for answering the underlying questions I had, whether to pursue writing our own parser/analyzer (using the paper you cited) or to use FRET in some way (via the standalone tool you pointed out).