Integration of FRET and WEST

🔍 Project Overview

This is Songyan Lai's final year project for his undergraduate degree in Computer Science at the National University of Ireland Maynooth.

• Contact:
  📧 laisongyan@foxmail.com
  📧 SONGYAN.LAI.2024@mumail.ie

• Supervisor: Prof. Rosemary Monahan
• Project Type: Research

---

🎯 Project Abstract

Development of safety-critical systems needs stringent requirements specification and verification to prevent catastrophic failure. This research accounts for syntac-tic and semantic differences between two formal verification tools: FRET, which generates Linear Temporal Logic (LTL) from natural language requirements; WEST, which works with Mission-time LTL (MLTL) formulas. This study cre-ates tool support for the automatic translation of the temporal logic generated by FRET to the temporal logic format expected by WEST. This translation is syntac-tically bridging and semantically preserving with bidirectional traceability to pri-mal requirements. Our solution utilizes regular expression-based mapping, varia-ble normalization, and mission-time interval translation to transform FRET's LTL specifications to WEST's MLTL syntax. A proof-of-concept JavaScript translator iteratively constructed through case studies, was incorporated as a feature within the FRET tool. Comparative validation in collaboration with the MU-FRET and WEST teams confirmed the efficacy of the framework. This research demon-strates enhanced reliability and efficiency in safety-critical requirements engineer-ing, with future research on semantic equivalence verification, cloud-native de-ployment, and human-centric interfaces. For more details, please refer to 'Final Report.pdf'.

---

📂 Repository Structure

FRET_to_WEST_MLTL_Converter

• Code Implementation
  JavaScript/HTML syntax converter developed through ~10 iterations
• Testing Files
  Archive of iterative development artifacts
• Deployment Status
  Integrated into MU-FRET platform

Research_Documents

• Key Analyses
  • The Motivation for Integration of WEST and FRET
  • Exploring WEST's Role in Temporal Logic Validation
• Progress Reports
  • Interim Report
  • Final Progress Report & Future Roadmap
• Case Studies
  • Formal-to-Runtime Verification Pipeline Implementation
  • WEST Validation Compliance with R2U2 Monitoring Specifications
  • Applied Integration Patterns in Aerospace Systems
• Other Supplementary Materials
  • Preliminary FRET/WEST comparative analysis
  • LTL Variants Survey Report
  • LAST V Operator Technical Brief
  • FRET-WEST-R2U2 Triad Study
  • FRET Operational Limitations Log
  • WEST Validation Scope Specification
  • WEST Team Discussion Report

---

✅ Completed Work

1. Automated Translation Framework A JavaScript translator that resynchronizes FRET's LTL to WEST's MLTL reduces manual translation time in industrial case studies. Furthermore, Innovations include Regex operator rewriting, finite-to-infinite trace emulation, and adaptive temporal granularity synchronization for real-time constraints.
2. Semantic-Preserving Heuristics Problem-domain-specific rule sets maintain logical equivalence during conflicts in mission-time intervals and nesting operator alignment. The ability to reconfigure resolution parameters minimizes quantization errors for safety-critical uses.
3. Toolchain Interoperability Mutual traceability provides linkages of MLTL results with FRETish requirements that are auditable and iteratively refineable. Further, open-source release induces co-operation amongst academia (Maynooth University, Iowa State University) and industry (KBR/NASA Ames Research Center).
4. Empirical Validation Case studies show 85% syntactic correctness and 80% semantic similarity.

---

🔮 Future Directions

1. Semantic Equivalence Verification Integrate SMT solvers (e.g., Z3) formally establish equivalence between FRET's LTL and MLTL translation.
2. Multi-Tool Redundancy Expand integration to runtime monitors (e.g., R2U2) and probabilistic checkers (e.g., PRISM).
3. Cloud-Native Scalability Execute containerized WEST instances on AWS/Azure for mission-scale verification.
4. Human-Centric Interfaces Develop AI-enabled annotation tools to map validation errors back to FRETish requirements.

---

🔗 Collaborators

Acknowledgments. We extend our gratitude to the original NASA FRET development team and the WEST team for their foundational work, and to Oisin Sheridan (Maynooth University) and Zili Wang (Iowa State University) for their technical guidance and collaborative support in bridging FRET and WEST.

NASA Vision Statement “To reach for new heights and reveal the unknown, so that what we do and learn will benefit all humankind.”

• NASA
• NASA FRET
• MU-FRET
• VALU3S
• WEST Tool

---

📚 Literature Review

1. Temporal Logic Foundations
   Pnueli (1977) LTL → MLTL extensions (Rozier 2020)
2. Verification Tools
   NASA FRET → MU-FRET safety adaptations
3. WEST Validation
   Elwing et al. (2024) syntax flexibility analysis

Last Updated: April 2025