Skip to content

Commit 9a6f971

Browse files
Akshay Rajhansclaude
Akshay Rajhans
and
claude
committed
Add fret-to-simulink — FRET requirements to Simulink RT and TA blocks
Translates NASA FRET temporal-logic requirements into Requirements Table blocks (for SLDV formal analysis) and Test Assessment blocks (for runtime verification). Validated on 122 requirements across FSM, Liquid Mixer, and LMCPS benchmarks — 15/15 RT models and 15/15 TA models compile successfully. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
1 parent 892e6cc commit 9a6f971

14 files changed

Lines changed: 3691 additions & 0 deletions

‎Packages/fret-to-simulink/GETTING-STARTED.md‎

Lines changed: 160 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,160 @@
1+
# Getting Started
2+
3+
This guide shows how to try the FRET-to-Simulink translator with example requirements.
4+
5+
## Example 1: FSM Case Study (FRET JSON → RT + TA)
6+
7+
The LMCPS benchmark provides 10 Simulink&reg; models with natural-language requirements created by Lockheed Martin Skunk Works. The models and requirements are [publicly available](https://github.com/hbourbouh/lm_challenges). This example uses the Finite State Machine (Challenge 1) with 13 FRETish requirements.
8+
9+
### Setup
10+
11+
```bash
12+
git clone https://github.com/hbourbouh/lm_challenges.git
13+
```
14+
15+
### Step 1: Export from FRET
16+
17+
In FRET, export the FSM project using "Export with variables" to produce `fsm_reqts_and_vars.json`. This file contains both the requirements (with compiled semantics) and the variable mapping (Input/Output/Internal types with constant assignments).
18+
19+
### Step 2: Convert to Requirements Table
20+
21+
```matlab
22+
addpath('helpers');
23+
rtBlk = fretJsonToRT('fsm_reqts_and_vars.json', 'FSM_RT');
24+
```
25+
26+
The function will report:
27+
- Number of requirements loaded and converted
28+
- Which requirements were skipped (e.g., unsupported templates)
29+
- Symbols added to the RT block
30+
31+
### Step 3: Run SLDV Analysis
32+
33+
```matlab
34+
opts = sldvoptions;
35+
opts.Mode = 'DesignErrorDetection';
36+
[status, files] = sldvrun('FSM_RT', opts);
37+
```
38+
39+
### Step 4: Convert to Test Assessment Block
40+
41+
```matlab
42+
taBlk = fretJsonToTA('fsm_reqts_and_vars.json', 'FSM_TA');
43+
```
44+
45+
### Step 5: Verify Against Model
46+
47+
```matlab
48+
open_system('fsm_12B');
49+
sltest.harness.create('fsm_12B/fsm', ...
50+
'Name', 'FRET_TA_Harness', ...
51+
'SeparateAssessment', true);
52+
```
53+
54+
Then populate the harness TA block with the generated assessments and run the test.
55+
56+
---
57+
58+
## Example 2: LMCPS Full Benchmark (97 Requirements, 13 Components)
59+
60+
The full LMCPS benchmark contains 97 requirements across 10 challenge sets and 13 FRET components. Because the JSON contains multiple `component_name` values, the pipeline creates a separate model per component by default.
61+
62+
### Step 1: Convert to Requirements Tables
63+
64+
```matlab
65+
addpath('helpers');
66+
rtBlks = fretJsonToRT('LM_requirements.json', 'LMCPS_RT');
67+
```
68+
69+
This creates 13 models: `LMCPS_RT_Autopilot.slx`, `LMCPS_RT_Euler.slx`, `LMCPS_RT_Tustin_Integrator.slx`, etc.
70+
71+
### Step 2: Compile and Validate
72+
73+
```matlab
74+
% Verify all models compile (Update Diagram)
75+
models = dir('LMCPS_RT_*.slx');
76+
for i = 1:numel(models)
77+
mdlName = models(i).name(1:end-4);
78+
load_system(mdlName);
79+
set_param(mdlName, 'SimulationCommand', 'update');
80+
close_system(mdlName, 0);
81+
end
82+
```
83+
84+
### What to expect
85+
86+
- 97 requirements loaded, 71 renderable to RT, 26 skipped
87+
- Skipped reasons: external function calls, complex `prev()` expressions, `persisted()` temporal operators, persistence patterns
88+
- 13 separate models created (one per FRET component)
89+
- All 13 models compile successfully
90+
- Vector signals (e.g., NLGuidance) automatically get correct dimensions
91+
- Dot products rewritten as transpose form for scalar postconditions
92+
93+
---
94+
95+
## Example 3: LiquidMixer Case Study (Single Component)
96+
97+
The LiquidMixer case study has 12 requirements in a single component. Since there's only one `component_name`, the pipeline creates a single model regardless of the `PerComponent` setting.
98+
99+
### Convert
100+
101+
```matlab
102+
rtBlk = fretJsonToRT('LM_reqts_and_vars.json', 'LiquidMixer_RT');
103+
```
104+
105+
### What to expect
106+
107+
- 12 requirements loaded, 9 renderable to RT, 3 TA-only (`weak_until` patterns)
108+
- Single model created: `LiquidMixer_RT.slx`
109+
- Compiles successfully
110+
111+
---
112+
113+
## FRET JSON Format
114+
115+
The input JSON must have this structure (FRET's "Export with variables" format):
116+
117+
```json
118+
{
119+
"requirements": [
120+
{
121+
"reqid": "REQ-001",
122+
"fulltext": "the controller shall always satisfy output >= 0",
123+
"semantics": {
124+
"scope": {"type": "null"},
125+
"condition": "null",
126+
"timing": "always",
127+
"post_condition": "output >= 0",
128+
"component_name": "controller"
129+
}
130+
}
131+
],
132+
"variables": [
133+
{
134+
"variable_name": "output",
135+
"idType": "Output",
136+
"dataType": "double"
137+
},
138+
{
139+
"variable_name": "THRESHOLD",
140+
"idType": "Internal",
141+
"assignment": "10.0",
142+
"dataType": "double"
143+
}
144+
]
145+
}
146+
```
147+
148+
Key points:
149+
- `Internal` variables with `assignment` values are mechanically substituted (constant replacement)
150+
- `Input` variables become RT Input symbols
151+
- `Output` variables become RT Input symbols with `IsDesignOutput = true`
152+
- The `semantics` field must contain FRET's compiled formalization output
153+
154+
---
155+
156+
## References
157+
158+
1. [NASA FRET](https://github.com/NASA-SW-VnV/fret) — Formal Requirements Elicitation Tool
159+
2. [LMCPS Benchmark](https://github.com/hbourbouh/lm_challenges) — Lockheed Martin Cyber-Physical Systems challenges
160+
3. [Simulink Agentic Toolkit](https://github.com/matlab/simulink-agentic-toolkit) — MCP server, tools, and skills for AI coding agents working with MATLAB and Simulink

‎Packages/fret-to-simulink/README.md‎

Lines changed: 122 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
# FRET to Simulink Translator
2+
3+
Translates [NASA FRET](https://github.com/NASA-SW-VnV/fret) temporal-logic requirements into Simulink&reg; verification artifacts — Requirements Table blocks for formal analysis with Simulink&reg; Design Verifier&trade;, and Test Assessment blocks for simulation-based runtime verification with Simulink&reg; Test&trade;.
4+
5+
Unlike [CoCoSim](https://github.com/NASA-SW-VnV/CoCoSim), which generates Verification Subsystem blocks with Proof Objectives for SLDV property proving, this pipeline targets Simulink's newer native artifacts — Requirements Table blocks (R2022a+) and Test Assessment blocks — enabling SLDV completeness/consistency analysis (Design Error Detection) and Simulink Test runtime verification workflows.
6+
7+
## Requirements
8+
9+
| Dependency | Required |
10+
|---|---|
11+
| MATLAB R2023a or later | Yes |
12+
| Simulink | Yes |
13+
| Requirements Toolbox&trade; | Yes |
14+
| Simulink Test | Yes (for Test Assessment blocks) |
15+
| Simulink Design Verifier | Optional (for formal analysis of RT blocks) |
16+
17+
## Quick Start
18+
19+
```matlab
20+
addpath("path/to/fret-to-simulink/helpers")
21+
22+
% Single-component project → one model with one RT block
23+
rtBlk = fretJsonToRT("fsm_reqts_and_vars.json")
24+
25+
% Multi-component project → one model per component (default)
26+
rtBlks = fretJsonToRT("LM_requirements.json", "LMCPS_RT")
27+
28+
% Multi-component project → merged into a single model
29+
rtBlk = fretJsonToRT("LM_requirements.json", "LMCPS_RT", PerComponent=false)
30+
31+
% Test Assessment block
32+
taBlk = fretJsonToTA("fsm_reqts_and_vars.json")
33+
```
34+
35+
When the FRET JSON contains multiple `component_name` values (common with multi-model benchmarks like LMCPS), `fretJsonToRT` creates a separate Simulink model per component by default. This avoids cross-component symbol conflicts and ensures each model can be independently analyzed with SLDV. Set `PerComponent=false` to merge all requirements into one model.
36+
37+
The pipeline loads the FRET JSON, converts each requirement through `fretToSpec`, routes to RT (invariant patterns) or TA (temporal patterns) based on renderability, creates the Simulink model(s), and reports conversion statistics.
38+
39+
For step-by-step examples, see **[GETTING-STARTED.md](GETTING-STARTED.md)**.
40+
41+
AI coding agents with access to the [Simulink Agentic Toolkit](https://github.com/matlab/simulink-agentic-toolkit) MCP server can call the helpers directly via `evaluate_matlab_code`.
42+
43+
## How It Works
44+
45+
```
46+
FRET JSON --> fretToSpec() --> reqCreateSpec struct --> reqCheckRenderability()
47+
|-- RT-renderable --> reqRenderToRT() --> RT block
48+
'-- TA-renderable --> reqRenderToTA() --> TA block
49+
```
50+
51+
The `fretToSpec` adapter handles:
52+
- SMV-to-MATLAB syntax conversion (`!` to `~`, `&` to `&&`, `=` to `==`)
53+
- Bi-implication expansion (`<=>` to conjunction of implications)
54+
- Implication splitting (`guard -> prop` to precondition/postcondition)
55+
- Constant substitution from FRET variable mapping (Internal variables)
56+
- FRET function mapping (`absReal` to `abs`, `preBool` to `prev`, `median` expansion)
57+
- FTP (First Time Point) sentinel handling
58+
59+
The TA pipeline uses **if-guard semantics**: guarded requirements emit `if guard; verify(response); end` so that unexercised requirements show UNTESTED (not vacuous PASS), matching the structured assessment editor behavior.
60+
61+
## Supported FRET Templates
62+
63+
| Template Key | Pattern | RT | TA | Notes |
64+
|---|---|---|---|---|
65+
| `null,null,always` | Unconditional invariant | Y | Y | Implication splitting |
66+
| `in,null,always` | Scoped invariant | Y | Y | scope_mode as guard |
67+
| `null,regular,always` | Persistent obligation (edge) | - | Y | Temporal persistence |
68+
| `null,holding,always` | Persistent obligation (level) | - | Y | |
69+
| `null,regular,immediately` | Edge-triggered immediate | Y | Y | RT uses `prev()` pattern |
70+
| `in,null,immediately` | Scope entry immediate | Y | Y | |
71+
| `in,regular,immediately` | Scoped edge-triggered | Y | Y | |
72+
| `null,holding,immediately` | Level-triggered immediate | Y | Y | |
73+
| `null,regular,next` | Next-step response | - | Y | P at t+1 |
74+
| `null,regular,within` | Bounded response | - | Y | |
75+
| `null,null,within` | Unconditional bounded | - | Y | |
76+
| `null,null,for` | Duration constraint | - | Y | |
77+
| `null,regular,until` | Until response | - | Y | |
78+
| `null,null,eventually` | Eventual satisfaction | - | Y | |
79+
| `null,null,never` | Negated invariant | Y | Y | |
80+
81+
## API
82+
83+
| Function | Description |
84+
|---|---|
85+
| `fretJsonToRT(jsonFile, modelName, NV)` | One-call pipeline: FRET JSON to Requirements Table block(s) |
86+
| `fretJsonToTA(jsonFile, modelName, NV)` | One-call pipeline: FRET JSON to Test Assessment block |
87+
| `fretToSpec(id, nl, semantics, vars)` | Convert FRET semantics to reqCreateSpec struct |
88+
| `reqCreateSpec(id, nl, pattern, NV)` | Create a requirement specification struct |
89+
| `reqRenderToRT(spec)` | Render a spec as RT precondition/postcondition |
90+
| `reqRenderToTA(spec)` | Render a spec as TA trigger/response configuration |
91+
| `reqCheckRenderability(spec)` | Check which targets (RT, TA) a spec supports |
92+
| `reqRenderStructuredEnglish(spec)` | Render a spec as human-readable Structured English |
93+
94+
### `fretJsonToRT` Name-Value Options
95+
96+
| Option | Default | Description |
97+
|---|---|---|
98+
| `ReqFilter` | `{}` | Cell array of reqids to include (empty = all) |
99+
| `Tolerance` | `0` | Numeric tolerance for double equality |
100+
| `SLDVReady` | `true` | Configure model for SLDV (fixed-step discrete solver) |
101+
| `PerComponent` | `true` | Create one model per FRET component |
102+
103+
## Validation
104+
105+
Validated on case studies from the [NASA FRET repository](https://github.com/NASA-SW-VnV/fret/tree/master/caseStudies) and the [LMCPS benchmark](https://github.com/hbourbouh/lm_challenges):
106+
107+
| Case Study | Total | RT Rendered | RT Compile | TA Rendered | TA Compile |
108+
|---|---|---|---|---|---|
109+
| FSM (Finite State Machine) | 13 | 11 | 1/1 | 13 | 1/1 |
110+
| Liquid Mixer | 12 | 9 | 1/1 | 12 | 1/1 |
111+
| LMCPS (all 10 challenges) | 97 | 71 | 13/13 | 74 | 13/13 |
112+
| **Total** | **122** | **91** | **15/15** | **99** | **15/15** |
113+
114+
Skipped requirements use features not currently expressible: external function calls (`mag`, `dot`, `det_3x3`), `prev()` with complex expressions, or `persisted()` temporal operators. Each LMCPS component produces a separate model; all compile and pass validation (Update Diagram). See [SUPPORTED-PATTERNS.md](SUPPORTED-PATTERNS.md) for the full pattern coverage matrix.
115+
116+
## References
117+
118+
1. [NASA FRET](https://github.com/NASA-SW-VnV/fret) — Formal Requirements Elicitation Tool
119+
2. [LMCPS Benchmark](https://github.com/hbourbouh/lm_challenges) — Lockheed Martin Cyber-Physical Systems challenges
120+
3. [Simulink Agentic Toolkit](https://github.com/matlab/simulink-agentic-toolkit) — MCP server, tools, and skills for AI coding agents working with MATLAB and Simulink
121+
4. C. Menghi, E. Balai, D. Valovcin, C. Sticksel, A. Rajhans, "Completeness and Consistency of Tabular Requirements: an SMT-Based Verification Approach," *IEEE Transactions on Software Engineering*, vol. 51, no. 2, Feb. 2025. [[IEEE](https://ieeexplore.ieee.org/document/10844918)]
122+
5. A. Rajhans, A. Mavrommati, P. J. Mosterman, and R. G. Valenti, "Specification and Runtime Verification of Temporal Assessments in Simulink," *21st International Conference on Runtime Verification (RV)*, 2021. [[PDF](https://www.mathworks.com/content/dam/mathworks/conference-or-academic-paper/specification-and-runtime-verification-of-temporal-assessments-in-simulink.pdf)]

‎Packages/fret-to-simulink/SUPPORTED-PATTERNS.md‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
# Supported FRET Patterns
2+
3+
This document describes which FRET requirement patterns translate to Simulink&reg; Requirements Table (RT) and Test Assessment (TA) blocks, and which are currently unsupported.
4+
5+
## Summary
6+
7+
| Benchmark | Total Reqs | RT Rendered | TA Rendered |
8+
|-----------|-----------|-------------|-------------|
9+
| LMCPS | 97 | 71 (73%) | 74 (76%) |
10+
| FSM | 13 | 11 (85%) | 13 (100%) |
11+
| Liquid Mixer | 12 | 9 (75%) | 12 (100%) |
12+
13+
## Supported Patterns
14+
15+
| Pattern | RT | TA | Notes |
16+
|---------|----|----|-------|
17+
| Invariant (always P) | Yes | Yes | Maps to unconditional postcondition / verify() |
18+
| Guarded invariant (if G then P) | Yes | Yes | Precondition + postcondition / if-guard + verify() |
19+
| Trigger-response (when T then P) | No | Yes | TA uses step transitions; RT lacks trigger semantics |
20+
| Edge trigger (when T becomes true) | No | Yes | TA uses hasChangedTo() or manual edge detection |
21+
| Duration trigger (T holds for N sec) | No | Yes | TA uses duration() >= N |
22+
| Response with delay (within N sec) | No | Yes | TA uses after(N, sec) return transitions |
23+
| Weak-until response (P until Q) | No | Yes | TA models via return transition on Q |
24+
| Hold-at-least response (P for >= N) | No | Yes | TA uses after(N, sec) for minimum hold |
25+
| prev(symbol) | Yes | Yes | RT uses prev() natively; TA uses Local variable pattern |
26+
| Boolean operators (and/or/not) | Yes | Yes | Mapped to &/\|/~ |
27+
| Arithmetic comparisons | Yes | Yes | Direct translation |
28+
| Implication (A => B) | Yes | Yes | Expanded to ~A \| B |
29+
| Tolerance equality (abs(x-y) < tol) | Yes | Yes | Optional via Tolerance parameter |
30+
31+
## Unsupported Patterns
32+
33+
| Pattern | RT | TA | Reason |
34+
|---------|----|----|--------|
35+
| persisted(N, expr) | Skip | Skip | FRET temporal operator with no direct Simulink equivalent. Would require counter-based state machine logic. |
36+
| prev(complex_expr) | Skip | Skip | Both RT and TA only support prev() on a single symbol name, not expressions like prev(A + B) or nested prev(prev(x)). |
37+
| External function calls (det_3x3, mag) | Skip | Skip | Requires extrinsic MATLAB function definitions that are not part of the FRET export. |
38+
| Massive nested pre() chains | Skip | Skip | Caught by complex-prev filter. Encodings like neural network weight tables are not expressible in RT/TA. |
39+
40+
## TA-Specific Implementation Details
41+
42+
### prev() Handling
43+
44+
TA Input-scoped symbols do not support the `prev()` operator. The pipeline creates Local variables (`prev_<name>`) with `DataType=double` and `InitialValue=0`, rewrites `prev(x)` to `prev_x` in all expressions, and appends `prev_x = x;` to every step action.
45+
46+
### Vector Signals
47+
48+
Signal dimensions are inferred from indexing patterns (e.g., `x(3)` implies size >= 3) and propagated through multiplications. All Input symbols receive explicit `Size` values since TA cannot infer dimensions from unconnected inports. Vector-vector multiplications are rewritten as dot products (`A' * B`) to produce scalar verify() expressions.
49+
50+
### Edge Detection
51+
52+
Simple triggers on bare identifiers use `hasChangedTo(signal, true)`. Compound trigger expressions (containing operators or arithmetic) use a manual edge-detection pattern with `cur_trig_N` and `prev_trig_N` Local variables.
53+
54+
## RT-Specific Implementation Details
55+
56+
### Design Outputs
57+
58+
RT requires at least one symbol marked as a Design Output. The pipeline infers outputs from postcondition structure: symbols that appear in postconditions but not directly in preconditions (outside prev()) are candidates.
59+
60+
### prev() Handling
61+
62+
RT supports `prev()` natively on Input symbols. Symbols used in prev() receive `InitialValue = '0'` to satisfy the RT block requirement for initial conditions.
63+
64+
### Vector Signals
65+
66+
Same inference as TA: indexing patterns determine size, multiplication propagates dimensions. The RT API uses `sym.Size = 'N'` directly. Vector-vector multiplications are rewritten as `A' * B`.

0 commit comments

Comments
 (0)