FORMAL SPECIFICATION OF ENVIRONMENTAL REQUIREMENTS IN AUTOMATED DRIVING SYSTEMS: A FRET-DRIVEN APPROACH

Abstract

The present thesis introduces a complete process that enables researchers to convert informal environmental requirements that apply to autonomous driving systems into formal specifications that can be analyzed and verified through official methods. The FRAV regulatory framework was used to extract 25 environmental requirements, which were processed into FRETish formal representation before being converted into diagrammatic semantics and temporal logic formats, which enable automated verification. The proposed workflow enables complete traceability throughout the process because it includes variable mapping and predicate abstraction and multiple backend export capabilities, which include LTL and SMT, thus supporting both design-time model checking and runtime monitoring. The study employed semantic and structural completeness, ambiguity and consistency metrics to assess FRET-based formalization, which demonstrated that its semantic comprehension and structural integrity improved compared to natural-language requirements, while it unveiled hidden assumptions that needed to be addressed before formal verification could proceed. The research demonstrates that diagrammatic semantics improve understanding for stakeholders, while formal encodings deliver exact specifications that machines can verify without altering the original purpose. The research demonstrates that combining requirements engineering with formal methods improves the safety-critical environmental requirements of autonomous systems via better quality and accurate traceability, and improved ability to verify requirements.