#4355 Solver for Formal Requirements Compliance Checking
#4355 Solver for Formal Requirements Compliance Checking #4355 Give tools like SAT and SMT Solvers, could a similar purpose tool be developed to "prove" a software planning and/or development document complies with a set of formal requirements? The short answer is yes , and in the world of high-stakes engineering—like NASA’s Safety and Mission Assurance (S&MA)—this is often referred to as Formal Specification and Automated Reasoning . While SAT (Satisfiability) and SMT (Satisfiability Modulo Theories) solvers are traditionally used to verify code or circuit logic, they are increasingly being applied to the "left side" of the V-model: the requirements and design phase. Here is how a tool for "proving" document compliance would function, the logic required, and the hurdles involved. 1. The Logic: Transforming Text into Predicates To "prove" compliance, you cannot work with raw English. You must translate the Formal Requirements (the "Ru...