Structured Language Requirement Analyzer
Requirements engineering is a critically important and error-prone phase of any product development effort. When developing system requirements across teams, defects are often created in the form of logical contradictions, over-complexity and inconsistency of entity names. The following is a demonstration of a technique to interpret specifications and automatically identify such defects.
The tool works by first parsing strings according to a context-free grammar, then performing simplification tactics over the parsed entities using an SMT solver (Z3). The solver leverages an understanding of propositional logic and integer mathematics to identify contradictions and potential simplifications.
Tips: All sentences must contain a "shall" to separate actors and their actions. Preconditions are optional, but if used must start with either "if", "when" or "while". All expressions must have spaces between terms (e.g. X > 3, not X>3). Full grammar in BNF (terminals are in quotes):
sentence ::= actor shall responses | conditions actor shall responses conditions ::= condition | condition conditions condition ::= subordinator clauses | subordinator clauses 'then' clauses ::= subclauses | subclauses conjunction subclauses subclauses ::= subclause | subclause conjunction subclauses | subclauses conjunction subclause | '(' subclauses conjunction subclause ')' | '(' subclauses conjunction subclause ')' subclause ::= left_side comparator right_side responses ::= response | response conjunction responses response ::= 'yield' symbol | 'send' symbol 'to' entity | 'set' symbol '=' right_side subordinator ::= 'if' | 'while' | 'when' left_side ::= symbol right_side ::= symbol | number conjunction ::= 'and' | 'or' comparator ::= '=' | '!=' | '>' | '<' | '<=' | '>=' | 'is' | 'is not'
Feel free to reach out to me on LinkedIn with any questions.