Tutorial

This is a hands-on walk through the editors, from an empty folder to a report you could hand to a reviewer. We carry one running example, a vehicle's door alarm, through every feature: its requirements, the circuit that implements it, a simulation, the proofs and the counterexamples, proof certificates, MC/DC tests, the report, and the way in and out through Lustre and Python.

The example is made up, and small on purpose. A vehicle has doors, a speed sensor and a button for the driver:

• the alarm sounds when a door is open while the vehicle moves faster than 5 km/h, and stops when the driver acknowledges it, until a door is opened again;
• the doors stay locked when a passenger asks one to open while the vehicle moves, or did a step before.

Time goes in steps, as in the controllers the editors are made for: at each step the inputs take new values and the outputs are computed from them and from what the circuit remembers of the steps before.

Before you start

Have one of the three forms of the editors at hand (Installation): the VS Code extension, Intrepid Studio, or the demo. The steps are the same in all three; where they differ, the tutorial says so in tabs, like these:

VS CodeIntrepid StudioThe demo

Open an empty folder (File › Open Folder…). The Intrepid icon in the Activity Bar opens the editors' side bar.

Start the studio on a new folder:

intrepid-studio ./door-alarm

Open the demo in your browser. It starts with the door alarm's example already in the project.

The pictures are of Intrepid Studio. In VS Code, the editors are the same, in VS Code's colours, and the side bar is VS Code's.

The finished project

If you would rather look at the result first, or get stuck on the way, here are the files the tutorial ends with. Put them in a folder and open it:

• door-alarm.requirements.json, the requirements table;
• door-controller.intrepyd.json, the circuit of the controller;
• door_lock.lus, the Lustre model of the lock.

The steps

1. Requirements: a table of requirements, their formulas, and the circuits built from them.
2. Drawing a circuit: the controller, block by block, then structured into subsystems.
3. Simulating: stimuli, values on the canvas, the scope.
4. Verifying: assertions, a target, two counterexamples, a fix, an assumption, and two proofs.
5. Proof certificates: a proof anyone can check.
6. MC/DC tests: the tests of a decision, and of the requirements.
7. The report: a page per requirement, to print.
8. Lustre and Python: a Lustre model opened as a circuit, and a circuit exported as a Python program.