SpecForge – A Platform for Authoring Formal Specifications

# A Whirlwind Tour - SpecForge User Guide Source: [https://docs.imiron.io/v/0.5.10/en/tour.html](https://docs.imiron.io/v/0.5.10/en/tour.html) ## Keyboard shortcuts Press←or→to navigate between chapters PressSor/to search in the book Press?to show this help PressEscto hide this help ## SpecForge User Guide ## [A Whirlwind Tour](https://docs.imiron.io/v/0.5.10/en/tour.html#a-whirlwind-tour) This section is a quick introduction to SpecForge’s main capabilities through a hands\-on example\. We’ll explore how to write specifications in the Lilo language and analyze them using SpecForge’s VSCode extension\. ## [The Lilo Language: A Brief Introduction](https://docs.imiron.io/v/0.5.10/en/tour.html#the-lilo-language-a-brief-introduction) Lilo is an expression\-based temporal specification language designed for hybrid systems\. Here are the key concepts: **Primitive Types**:`Bool`,`Int`,`Float`, and`String` **Operators**: Standard arithmetic \(`\+`,`\-`,`\*`,`/`\), comparisons \(`==`,`<`,`\>`, etc\.\), and logical operators \(`&&`,`\|\|`,`=\>`\) **Temporal Operators**: Lilo’s distinguishing feature is its rich set of temporal logic operators: - `always φ`:`φ`is true at all future times - `eventually φ`:`φ`is true at some future time - `past φ`:`φ`was true at some past time - `historically φ`:`φ`was true at all past times These operators can be qualified with time intervals, e\.g\.,`eventually\[0, 10\] φ`means`φ`becomes true within 10 time units\. More operators[are available](https://docs.imiron.io/v/0.5.10/en/lilo-language.html#operators)\. **Systems**: Lilo specifications are organized into systems that group together: - `signal`s: Time\-varying input values \(e\.g\.,`signal temperature: Float`\) - `param`s: Non\-temporal parameters that are not time\-varying \(e\.g\.,`param max\_temp: Float`\) - `type`s: Custom types for structured data - `def`initions: Reusable definitions and helper functions - `spec`ifications: Requirements that should hold for the system A system file begins with a system declaration like`system temperature\_control`and contains all the declarations for that system\. For a comprehensive guide to the language, see the[Lilo Language](https://docs.imiron.io/v/0.5.10/en/lilo-intro.html)chapter\. ## [Running Example](https://docs.imiron.io/v/0.5.10/en/tour.html#running-example) We’ll use a temperature control system as our running example\. This example project is available in the[releases](https://imiron.io/specforge/releases/)\. The system monitors temperature and humidity sensors, with specifications ensuring values remain within safe ranges: ``` system temperature_sensor // Temperature Monitoring specifications // This spec defines safety requirements for a temperature sensor system import util use { in_bounds } signal temperature: Float signal humidity: Float param min_temperature: Float param max_temperature: Float #[disable(redundancy)] spec temperature_in_bounds = in_bounds(temperature, min_temperature, max_temperature) spec always_in_bounds = always temperature_in_bounds // Humidity should be reasonable when temperature is in normal range spec humidity_correlation = always ( (temperature >= 15.0 && temperature <= 35.0) => (humidity >= 20.0 && humidity <= 80.0) ) // Emergency condition - temperature exceeds critical thresholds spec emergency_condition = temperature < 5.0 || temperature > 45.0 // Recovery specification - after emergency, system should stabilize spec recovery_spec = always ( emergency_condition => eventually[0, 10] (temperature >= 15.0 && temperature <= 35.0) ) ``` The[VSCode extension](https://docs.imiron.io/v/0.5.10/en/vscode-extension.html)provides support for writing Lilo code, syntax highlighting, type\-checking, warnings, spec satisfiability, etc\.:  ## [Spec Analysis](https://docs.imiron.io/v/0.5.10/en/tour.html#spec-analysis) Once you’ve written specifications for your system, the SpecForge VSCode extension provides various analysis capabilities: - **Monitor**: Check whether recorded system behavior satisfies specifications - **Exemplify**: Generate example traces that satisfy specifications - **Falsify**: Search for counterexamples that violate specifications, relative to some model - **Export**: Convert specifications to other formats \(`\.json`,`\.lilo`, etc\.\) - **Animate**: Visualize specification behavior over time This can be done directly from within VSCode, or from within in a Jupyter notebook using the[Python SDK](https://docs.imiron.io/v/0.5.10/en/python-sdk.html)\. We will perform analyses directly in VSCode here\. The[VSCode guide](https://docs.imiron.io/v/0.5.10/en/vscode-extension.html)details all features in greater depth\. ### [Monitoring](https://docs.imiron.io/v/0.5.10/en/tour.html#monitoring) Monitoring checks whether actual system behavior, recorded in a data file, satisfies your specifications\. You provide recorded trace data, and SpecForge evaluates a specification against it\. Navigate to the spec selection screen, and click the`Analyse`button for the spec you want to monitor\.  After selecting a data file from the dropdown menu, click`Run Analysis`\. The result is an analysis monitoring tree for the specification:  The result for the whole specification is shown at the top\. Below this, you can drill down into sub\-expressions of the specification, to understand what makes the spec true or false at any given time\. Hovering over any of the signals will show a popup with an explanation of the result at that point in time, and will highlight relevant segments of sub\-expression result signals\. An analysis can be saved\. To do so, click the`Save Analysis`button, and choose a location to save the analysis\. You can then navigate to this analysis file and open it again in VSCode\. The analysis will also show up in the specification status menu, under the relevant spec\.  ### [Exemplification](https://docs.imiron.io/v/0.5.10/en/tour.html#exemplification) The`Exemplify`analysis generates example traces that demonstrate satisfying behavior\. This is useful for: - Understanding what valid system behavior looks like - Testing other components with realistic data - Creating animations  If the exemplified data does not behave as expected, the specification might be wrong and need to be corrected\. Exemplification can thus be used as an aid when authoring specifications\. ### [Falsification](https://docs.imiron.io/v/0.5.10/en/tour.html#falsification) If a model for the system is available, falsification can be used to see if the model behaves as expected, that is, according to specification\. First a falsifier must be registered in`specforge\.toml`, e\.g\. ``` [project] name = "automatic-transmission" source = "spec" [[system_falsifier]] name = "AT Falsifier" system = "transmission" script = "transmission.py" ``` Once this is done, the falsifier will show up in the`Falsify`analysis menu\. If a falsifying signal is found, the monitoring tree is show, to help understand how the model went wrong:  ### [Export](https://docs.imiron.io/v/0.5.10/en/tour.html#export) `Export`converts your specifications to other formats, to be used in other tools\. For example, if you want to export your specification to JSON format, choose`\.json`as the`Export type`\.  ## [Next Steps](https://docs.imiron.io/v/0.5.10/en/tour.html#next-steps) This tour covered the basics of what SpecForge can do\. The following chapters dive deeper into: - The full Lilo language \([Lilo Language](https://docs.imiron.io/v/0.5.10/en/lilo-language.html)\) - System definitions and composition \([Systems](https://docs.imiron.io/v/0.5.10/en/lilo-systems.html)\) - The Python SDK for programmatic access \([Python SDK](https://docs.imiron.io/v/0.5.10/en/python-sdk.html)\) [https://docs.imiron.io/v/0.5.10/en/license-modes.html](https://docs.imiron.io/v/0.5.10/en/license-modes.html)[https://docs.imiron.io/v/0.5.10/en/lilo-intro.html](https://docs.imiron.io/v/0.5.10/en/lilo-intro.html) [https://docs.imiron.io/v/0.5.10/en/license-modes.html](https://docs.imiron.io/v/0.5.10/en/license-modes.html)[https://docs.imiron.io/v/0.5.10/en/lilo-intro.html](https://docs.imiron.io/v/0.5.10/en/lilo-intro.html)