R2U2 Export for FRET - Contribution from Collins Aerospace

[aaurandt]

We are currently working on creating an R2U2 export feature for FRET.

One of the primary features that needs to be added is converting LTL to Mission-time Metric Temporal Logic (MLTL). MLTL is a variant of LTL over finite traces with temporal intervals that are bounded, closed, and discrete, and it is the logic that R2U2 natively reasons over (more information on R2U2 and MLTL is available here). It's also important to realize that R2U2 re-evaluates specifications for each time step of execution; therefore, each MLTL specification that R2U2 monitors has an implicit exterior Global operator.

We have added this conversion from FRETish to MLTL, although we are still investigating additional rewriting rules that may be applicable. (Note we are only focusing on future-time MLTL as specifications for aerospace systems are commonly expressed in future-time.) Here is an example within FRET:

The other primary feature is converting these MLTL formalizations and input variables into a C2PO specification file that R2U2 can reason over. For examples of C2PO specifications, please review our R2U2 Playground: https://r2u2.temporallogic.org/playground/ In the end, this R2U2 export option will produce the respective C2PO file:

As we work on this contribution, we will update this discussion. Once our contribution is complete, we will make a corresponding pull request for the FRET team to review.

[anmavrid]

Thanks Alexis for starting this discussion. This sounds great! We will start reviewing the information that you have provided.

Anastasia

[aaurandt]

We have also enabled viewing the MLTL in the WEST format (https://west.temporallogic.org/). A user will have to specify M (i.e., end of mission-time) before running the spec in WEST when applicable.

[aaurandt]

When mapping variables for R2U2 export, we do not allow variable data types of unsigned integer or single as R2U2 natively supports only signed integers and doubles. Additionally, R2U2 does not currently support functions; therefore, if there is a variable of Function type, the user will be blocked from exporting. If the variable is an internal variable, we also check that it matches R2U2's expected format before allowing a user to export.

When the R2U2 export feature is selected, a .zip folder with a .c2po specification file, a .map file, and a .csv file is downloaded.
The .map or .csv header is required to map the input signal vector into R2U2.

Here is the example output files for the Finite State Machine case study: