A Compositional Proof Framework for FRETish Requirements
summary
Formalization defines a new denotational semantics for Fretish and proves semantic equivalence between Fretish requirements and the MTL formulas Fret generates, all developed and checked in PVS theorem prover. The proof is compositional: 160 scope/condition/timing combinations reduce to a reusable set of about 20 lemmas, targets the past-time MTL fragment, finds two real bugs (an eventually case and a scope/timing combo) and yields an extensible, machine-checked generator.
AI-written summary · about