- Author
- Not stated
- Published
- Undated
- Kind
- Product documentation, a hands-on tour chapter
- Original
- docs.imiron.io/v/0.5.10/en/tour.html
- Subject
- Formal methods and proof
What it is
The page is a quick tour in a software user guide. It introduces Lilo and the SpecForge VSCode extension. It aims to show the main features through one running example.
What it says
- The guide calls Lilo an expression-based temporal specification language designed for hybrid systems.
- Lilo's distinguishing feature is its temporal operators, such as always, eventually, past and historically.
- Operators can take time intervals, such as becoming true within a window.
- A Lilo system groups signals, parameters, types, definitions and specifications.
- The running example is a temperature and humidity sensor with bounds and a recovery rule.
- SpecForge can monitor recorded data against a spec and show a tree of sub-expression results.
- Falsify searches for counterexamples to a spec, relative to a model.
What evidence it gives
The page gives one worked example in Lilo code. It describes each analysis in words. It does not report benchmarks, case studies or user results.
Interests and limits
The page comes from the vendor's own documentation, so it presents the product favourably. The text was read in full, but the screenshots were not viewed. No claim about speed, accuracy or real-world use is made. The tour shows basics only and points to later chapters.