SpecForge: A Framework for Formal Specification Authoring

Quick-Start Guide: A Whirlwind Tour This section provides a high-level overview of SpecForge's core functionality through a practical, hands-on demonstration. We will examine the creation of specifications using the Lilo language and their subsequent analysis via the SpecForge VSCode extension.

---

🌐 The Lilo Language: An Overview

Lilo is a temporal, expression-based specification language specifically engineered for hybrid systems.

Core Components

Lilo utilizes several fundamental building blocks to define system behavior:

⏳ Temporal Logic

The defining characteristic of Lilo is its suite of temporal operators, which allow developers to describe how properties evolve over time. Let $\phi$ represent a property:

• Always ($\square \phi$): $\phi$ must remain true for all future time steps.
• Eventually ($\diamond \phi$): $\phi$ must become true at least once in the future.
• Past: $\phi$ was true at some point in the previous timeline.
• Historically: $\phi$ has been true throughout the entire past.

These can be constrained by specific time windows. For example, $\diamond_{[0, 10]} \phi$ indicates that $\phi$ must occur within a duration of 10 time units.

🏗️ System Architecture

Specifications are encapsulated within system blocks. A system declaration (e.g., system temperature_control) organizes the following:

1. signal s: Values that fluctuate over time (e.g., signal temperature: Float).
2. param s: Constant, non-temporal parameters (e.g., param max_temp: Float).
3. type s: User-defined structured data types.
4. Definitions: Helper functions and reusable logic.
5. Specifications: The actual requirements the system must satisfy.

For more detail, refer to the full Lilo Language documentation.

---

🌡️ Running Example: Temperature Control

Consider a system designed to monitor environmental sensors. We want to ensure that temperature and humidity stay within safe operational limits.

system temperature_sensor 
// Specifications for monitoring temperature and humidity

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)

// Requirement: Temperature must always stay within bounds
spec always_in_bounds = always temperature_in_bounds 

// Requirement: Humidity must be between 20% and 80% if temperature is between 15 and 35
spec humidity_correlation = always ( 
    (temperature >= 15.0 && temperature <= 35.0) 
    => (humidity >= 20.0 && humidity <= 80.0) 
)

// Requirement: Define an emergency state when thresholds are breached
spec emergency_condition = temperature < 5.0 || temperature > 45.0 

// Requirement: After an emergency, the system must stabilize within 10 units
spec recovery_spec = always ( 
    emergency_condition => eventually[0, 10] (temperature >= 15.0 && temperature <= 35.0) 
)

The VSCode extension enhances this experience by providing manual checking automated type-checking, syntax highlighting, and satisfiability warnings.

---

🔍 Spec Analysis

Once your Lilo code is authored, the VSCode extension offers several powerful analysis tools:

1. Monitoring

Monitoring validates whether actual recorded system data adheres to your specifications.

• Process: Select the desired specification $\rightarrow$ Click Analyse $\rightarrow$ Choose a data file $\rightarrow$ Click Run Analysis.
• The Monitoring Tree: The result is displayed as a hierarchical tree. The root shows the overall status, while child nodes allow you to drill down into sub-expressions to pinpoint exactly where a spec failed.
• Interactivity: Hovering over signals provides a popup explanation and highlights the corresponding time segments in the result signals.
• Persistence: Use the Save Analysis button to store the results for future review in VSCode or the specification status menu.

2. Exemplification

This tool generates synthetic traces that satisfy the specification. This is vital for:

• Visualizing what "correct" behavior looks like.
• Creating test data for other system components.
• Validating the specification itself (if the generated trace looks wrong, the spec is likely flawed).

3. Falsification

Falsification attempts to find counterexamples that violate the spec, provided a system model exists. You must first register a falsifier in the specforge.toml file:

[project]
name = "automatic-transmission"
source = "spec"

[[system_falsifier]]
name = "AT Falsifier"
system = "transmission"
script = "transmission.py"

If a violation is discovered, SpecForge provides a monitoring tree to help diagnose the model's failure.

4. Export & Animation

• Export: Convert specs into other formats (e.g., .json) for use in external tooling.
• Animate: Visualize the specification's behavior over time. This is available directly in VSCode or via the Python SDK within a Jupyter notebook.

---

🚀 Next Steps

You have now completed the introductory tour of SpecForge.

• Understand Lilo basics
• Explore the VSCode extension
• Dive into advanced temporal logic
• Implement a custom falsifier
• Export specifications to JSON