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.