FTL-CFree: A Fuzzy Real-Time Language for Runtime Verification

This paper presents the functional specification language fuzzy temporal logic context free (FTL-CFree), a real runtime language designed to enable industry to model and verify complex scenarios. Such specification requirements demand the flexibility to manage manufacturing event correlations, performance constraints, and timing restrictions, such as holdups and delays. Moreover, this language enriches temporal logic expressiveness with random access to past values and fuzzy evolutionary semantics. Given a specific input trace, this interpretation not only aims to measure the degree of truth of an assertion, but also sets how it will evolve in the future if new trace suffixes are provided. As it is usually the case in runtime verification, the language provides for oracle generation, and so an automatic observable specification can be obtained from high-level requirements. To test the expressiveness and practical usefulness of FTL-CFree, the specifications of two industrial use cases are generated: 1) a batch plant in a glassworks; and 2) a manufacturing execution system.