Skip to content

FRET public release v3.0.0

Latest
Latest
Compare
Choose a tag to compare
@anmavrid anmavrid released this 27 Mar 22:26
· 28 commits to master since this release
v3.0.0
1cddd85

1. Probabilistic Requirement Specification and Formalization

  • Introduced support for probabilistic requirements, enabling the specification of uncertainty - crucial for autonomous systems.
  • Extended the FRETish language with a probability field for direct probabilistic constraint specification.
  • Automated the formalization of probabilistic requirements as Probabilistic Computational Tree Logic Star (PCTL*) formulas.
    • PCTL* formulas are generated in a compositional manner, promoting extensibility and maintainability of the tool.
    • The generated PCTL* formulas adhere to the syntax of the PRISM property specification language, facilitating connection with the PRISM and other probabilistic model checkers.

2. Requirement-Based Test Case Generation

  • Automated the test case generation from FRETish requirements based on test obligation formulas, leveraging the FLIP requirements coverage metric to ensure comprehensive testing.
  • Integrated two test generation engines:
    • Kind 2: for past-time LTL formulas
    • NuSMV: for future- and past-time LTL formulas.
  • Added multiple export options:
    • Test cases (from both Kind 2 and NuSMV) can be exported in JSON format.
    • Test obligation formulas, the core of the test generation process, can be exported in Lustre or SMV syntax.
  • Enabled visualization of NuSMV-generated tests using the FRET simulator (LTLSIM), to visually and interactively inspect and validate the generated tests.

3. Revamped Analysis Portal

  • Added a 'Complete' column to the variables mapping table for mandatory variable information specification.
  • Implemented asynchronous diagnosis of unrealizable results for improved efficiency.
  • Enhanced tooltip behavior for realizable requirement simulations.

4. Revamped LTLSIM Simulator

  • Enabled multi-trace display with varying lengths within a single window.
  • Added trace export/import functionality in JSON and CSV formats.
  • Improved trace annotation and selection features.
  • Enhanced integration for visualizing realizability counterexamples.
  • Included an hourglass cursor for visual feedback of NuSMV processing.

5. Installation & Infrastructure

  • Adopted Apache 2.0 licensing for FRET.
  • Improved robustness of realizability checking to accommodate JSON format variations across Kind 2 versions.
  • Updated .deb dependencies in Dockerfile for Ubuntu 24.04 compatibility.
  • Revised WSL installation guide with latest system requirements.
  • Bumped dependencies, including the nodegyp package.

6. User Manual & Documentation

  • Expanded and improved the user manual documentation.
  • Added Lockheed Martin case study requirements and a step-by-step test obligation generation guide for Lustre/Simulink.
Assets 2
Loading