Reference#

Introduction#

This reference provides a formal and complete description of the req language. It covers entity constructs, the expression language, traceability mechanisms, and compiler diagnostics, with syntax and examples for each.

This is not an introduction to req. Readers new to the language should start with the Overview section and the Getting started tutorial before consulting this reference.

This reference acts as the specification for the req language. It is the source of truth: any behavior in req tooling that contradicts this document can be considered a bug. Particularly, the reference specifies:

  • The formal syntax of the language

  • The semantics for each concept of the language.

Note that this reference is therefore a good starting point to understand the req-lang/reqtool implementation.

Only fully specified features are covered here. Draft or experimental functionality is not included. Features that are not yet implemented but fully specified have a special mention.

Contents:

Prerequisites#

The expression language covers a broad range of formal concepts. Familiarity with the following is helpful to make full use of it:

  • Systems engineering, particularly MBSE and languages such as SysML

  • Requirements engineering, particularly functional and physical decomposition

  • Formal logic, particularly LTL and FOL

  • Mathematics, particularly set theory

These are not strict prerequisites. Entity constructs and informal requirements can be used without any background in formal methods.

Conventions#

  • A mandatory property is expressed as an affirmative phrase, e.g. “The document starts with a package.” It should be read as “the document shall start with a package”, meaning any conforming implementation must respect the property.

  • An optional property is expressed as an affirmative phrase using the modal may, e.g. “The expression may have a type.” It should be read as “the expression may or may not have a type.” A conforming implementation must handle both cases.

  • The use of modals, can, must, should refer to actual specification property not language properties.

A syntax notation is used throughout this reference to describe the formal grammar of the language. It is intended to be more readable than BNF while remaining unambiguous:

  • LABEL (uppercase) represents a defined language concept

  • <LABEL_A | LABEL_B> represents a choice between two alternatives

  • LABEL? indicates zero or one occurrence, LABEL* zero or more, LABEL+ one or more

  • (X) indicates a grouping, that is meant to be used with cardinality specification above

  • All other tokens are literal

Terminology#

  • System means the SOI

  • Environment means anything outside of the system required to specify the system

  • Specification means a req file, containing the specification of the system and its environement