# The role of formalism in system requirements (full version)

Jean-Michel Bruel<EMAIL_ADDRESS>University of Toulouse, IRIT ,  Sophie
Ebersold<EMAIL_ADDRESS>University of Toulouse, IRIT ,  Florian
Galinier<EMAIL_ADDRESS>University of Toulouse, IRIT ,  Manuel
Mazzara<EMAIL_ADDRESS>Innopolis University ,  Alexandr Naumchev
<EMAIL_ADDRESS>Innopolis University and  Bertrand Meyer
<EMAIL_ADDRESS>Schaffhausen Institute of Technology and IRIT

###### Abstract.

A major determinant of the quality of software systems is the quality of their
requirements, which should be both understandable and precise. Most
requirements are written in natural language, good for understandability but
lacking in precision.

To make requirements precise, researchers have for years advocated the use of
mathematics-based notations and methods, known as “formal”. Many exist,
differing in their style, scope and applicability. The present survey
discusses some of the main formal approaches and compares them to informal
methods.

The analysis uses a set of 9 complementary criteria, such as level of
abstraction, tool availability, traceability support. It classifies the
approaches into five categories: general-purpose, natural-language,
graph/automata, other mathematical notations, seamless (programming-language-
based). It presents approaches in all of these categories, altogether 22
different ones, including for example SysML, Relax, Eiffel, Event-B, Alloy.

The review discusses a number of open questions, including seamlessness, the
role of tools and education, and how to make industrial applications benefit
more from the contributions of formal approaches.

This is the full version of the survey, including some sections and two
appendices which, because of length restrictions, do not appear in the
submitted version.

††publicationmonth: 11††journalyear: 2019

##  1\. Introduction

In a world where software pervades every aspect of our lives, a core issue for
the IT industry is how to guarantee the quality of the systems it produces.
Software quality is a complex and widely studied topic, but it is not hard to
provide a simple definition: quality means that the software does the right
things, and does them right. These “things” that a software system does are
known as its requirements. Not surprisingly, requirements engineering is a
core area of software engineering.

Both goals, doing the right things and doing things right, fundamentally
depend on the quality of the requirements: the requirements must define the
system so that it will satisfy user needs; and they must make it possible to
assess a candidate implementation against this definition, a task known as
_validation_ (as distinct from _verification_ , which assesses the internal
properties of the implementation).

Validation can only be effective if the requirements are precise. Precision in
science and technology is typically achieved by using mathematical methods and
notations, also known in software engineering as _formal_ methods and
notations. This survey examines the state of the art in applying such formal
approaches to software requirements, and perspectives for their further
development.

Precision is so important that an outsider to the field might assume that
_all_ software development starts with a formal description of the
requirements. This approach is by far not the standard today; most practical
projects, if they use explicit requirements at all, describe them informally,
either in the form of a natural-language “requirements document” or (in agile
methods) through individual “user stories”, also expressed in natural
language.

A number of _formal requirements methods_ also exist. The following sections
present some of them together with the supporting notations and tools, and
discuss their applicability as a replacement for, or complement to, the
dominant informal approaches.

A version of this article has been submitted for publication, omitting a few
sections and the appendices because of length restrictions. To maintain
consistency of numbering, the supplementary sections have special numbers such
as 4.1.A in the present full-length version.

###  1.1. Terminology: requirements versus specifications

“Formal _specification_ ” is a well-accepted concept, covered by various
survey articles (Tilley et al., 2005; Woodcock et al., 2009). The present
article surveys formal requirements. While it is generally accepted that the
concepts of specification and requirements are both distinct and related,
there exist – even within a single normative source such as the Software
Engineering Body of Knowledge (Bourque and Fairley, 2014) – varying
definitions of the difference. This article will rely on the following
definition of the distinction, with which we believe many knowledgeable
professionals would agree.

First, what is common to requirements and specifications: both describe the
“what” of a system or system element — its purpose and the constraints to
which it is submitted — rather than the “how”, which is the responsibility of
other software engineering tasks, _design_ and _implementation_.

As to the difference, it is one of purpose and scope:

  * •

A specification describes the _technical properties_ of a system, or often
some part of a system. For example, the rendering engine of a Web browser must
display any given HTML text in a certain way. A specification will describe
the desired properties of this rendering.

  * •

Requirements describe the properties of a system or system element as relevant
to its human users, or more generally its _environment_. (This generalization
is necessary since not all systems have a direct human “user”: many, such as
the engine of a car, serve the purpose of another system, in this case the car
as a whole.) For example, the requirements for a Web browser describe the
functionality that it provides to its users and the constraints on this
functionality.

This definition indicates why the distinction between requirements and
specifications cannot be absolute: to produce the requirements of a complex
system, it will be necessary to decompose them into sub-requirements of its
components, and the further you go into this decomposition the more detailed
and technical the requirements will become, getting closer to specifications.
Even if not absolute, the distinction is useful. This article focuses on
formal approaches to requirements, applicable to entire systems and covering
the properties directly relevant to the its users and environment. While there
have been systematic studies of formal specifications, formal requirements are
a less well-explored topic. The present article is an attempt to fill this
gap.

###  1.2. Terminology: “specification”

Two further observations on terminology will help avoid confusion:

  * •

The verb “to specify” is in common English use to mean “to describe precisely”
or “to include a mention of”. Such use is applicable to requirements too, as
in “Your implementation ignores this case, but the requirements document
specifies that it must be reported as an error!”. It would be cumbersome to
deprive ourselves from such standard usage, as long as it does not imply any
confusion with the term “specification” in its technical sense discussed
above.

  * •

Following the standard practice of the requirements literature, this article
uses “a _requirement_ ” as the description of a particular property of a
system and “the _requirements_ ” as the collection of every such individual
“requirement” for a system. “Requirements” here is not just the plural of
“requirement” but a concept on its own, often understood as an abbreviation
for “the requirements document”. In this discussion, “requirements” denotes
that collective concept. When the emphasis is on one or more specific
“requirement” the phrasing will reflect it clearly, as in “requirement #25” or
“the following three requirement _elements_ ” etc.

##  2\. Running example

To illustrate and compare the approaches surveyed, it is useful to rely on a
common example. A well-known survey that used such an example is Wing’s 1988
study of specifications of a simple library system (Wing, 1988). To reflect
the challenges of today’s demanding IT applications, we need a more difficult
example. This article uses the Landing Gear System for airplanes (LGS), a case
study (Boniol and Wiels, 2014) that has received wide attention in the
requirements literature (including in the authors’ own previous work (Naumchev
et al., 2019)). The LGS is a a complex, critical system for which the
requirements involve diverse stakeholders and many fields of expertise.

Physically, an LGS consists of the landing set, a gear box that stores the
gear in retracted position, and a door attached to the box. The door and gear
are independently activated by a digital controller. The controller reacts to
changes of position of a handle by initiating either gear extension or
retraction process. In other words, the controller must align in time the
events of changing the handle’s position and sending commands to the door and
the gear actuators: doors are opened and closed and gears are either moving
out (extension) or moving in (retraction). One may express these rules, still
in natural language but more precisely, as follows (all applicable to “command
line” mode):

  * •

(R11bis) If the landing gear command handle has been pushed down and stays
down, then eventually the gears will be locked down and the doors will be seen
closed.

  * •

(R12bis) If the landing gear command handle has been pushed up and stays up,
then eventually the gears will be locked retracted and the doors will be seen
closed.

  * •

(R21) If the landing gear command handle remains in the down position, then
retraction sequence is not observed.

  * •

(R22) If the landing gear command handle remains in the up position, then
outgoing sequence is not observed.

We will see how to express some of these properties in some of the approaches
surveyed.

##  3\. Classifying approaches to requirements

This section introduces a classification of approaches into five categories
(3.1), introduces the approaches retained and why they were retained (3.2),
and lists the assessment criteria (3.3)

###  3.1. The classification

Approaches fall into five categories based on how they express requirements:

  * •

Natural language category approaches express requirements in English or
another human language, although they can restrict the degree of “naturalness”
of the text.

  * •

Semi-formal approaches codify the form of requirements, in effect defining a
precise requirements language, which is neither a mathematical notation (as in
the next two categories) nor derived from an programming language (as in the
last category).

  * •

Automata, graphs approaches rely on notations based on automata or graph
theory. They usually provide graphical support and may leave the mathematical
basis implicit since graphs, in particular, can be used a diagrammatic tool
without deep mathematical knowledge.

  * •

Mathematical approaches rely on mathematical formalisms other than those of
the previous category.The theoretical basis is, generally, mathematical logic.

  * •

Seamless approaches integrate requirements closely with other software tasks
(design, implementation…), using a programming language as notation.

###  3.2. Selection criteria and list of approaches surveyed

The field of requirements engineering is rich with methods and tools. Any
survey must involve a choice and, inevitably, some subjectivity. The present
discussion has retained approaches that meet one or more of the following
criteria:

  * •

Widely used (as in the case of commercially available tools such as Doors).

  * •

Widely publicized.

  * •

Influential.

  * •

Possessing, in the authors’ view, other distinctive characteristics that
warrant discussion.

Note that some of the authors have (separately) been involved in three of the
methods reviewed, Relax (4.1.2), multirequirements (4.5.1), and seamless
object-oriented requirements (SOOR) (4.5.2).

Table 1 lists the approaches retained for this survey. The references to the
corresponding publications also appear here. When these publications do not
give an approach an explicit name, we devised one carrying the central
concept, such as Requirements Grammar, and marked it with an asterisk*.

Name | Category | References | Section
---|---|---|---
Requirements Grammar* | Natural language | (Scott and Cook, 2004) | 4.1.1
Relax | (Whittle et al., 2009) | 4.1.2
Stimulus | (Jeannet and Gaucher, 2015) | 4.1.3
NL to OCL* | (Hähnle et al., 2002) | 4.1.A
NL to STD* | (Aceituna et al., 2011) | 4.1.B
NL to OWL* | (Li et al., 2015) | 4.1.4
Doors | Semi-formal | (IBM, 2015) | 4.2.1
Reqtify | (Systems, 2016) | 4.2.1
KAOS | (van Lamsweerde, 2001) | 4.2.2
URN | (Amyot, 2003) | 4.2.A
SysML | ((OMG), 2007) | 4.2.3
URML | (Berenbach et al., 2012) | 4.2.B
Petri Nets | Automata- or graph-based | (Peterson, 1977) | 4.3.A
Statecharts | (Harel, 1987) | 4.3.1
Problem Frames | (Jackson, 2001) | 4.3.2
FSP/LTSA | (Magee and Kramer, 1999) | 4.3.3
FORM-L | (Nguyen, 2015) | 4.3.4
Event-B | Mathematical notation | (Abrial, 2010) | 4.4.1
VDM | (Bjørner and Jones, 1978) | 4.4.A
Process Algebra | (Hoare, 1978; Milner, 1982) | 4.4.B
Alloy | (Jackson, 2006) | 4.4.2
Tabular Relations | (Parnas, 2011) | 4.4.C
Multirequirements | Seamless | (Meyer, 2013; Naumchev and Meyer, 2017) | 4.5
Table 1. Requirements approaches surveyed

###  3.3. Criteria for assessing approaches

The matter of assessing the quality of requirements has received significant
attention, not only in the research literature (Schneider and Buede, 2000;
Soares et al., 2011) but also in industry standards, from the venerable IEEE
830-1993 (IEEE, 1998) to the more recent ISO/IEC/IEEE 29148-2011 (IEEE, 2011).
They list such criteria as traceability, verifiability, consistency,
justifiability and completeness.

For the present discussion, we need criteria one notch higher in the
abstraction scale since the goal is to evaluate not the quality of
requirements but approaches to requirements engineering. The discussion
retains nine criteria for assessing requirements approaches.

Criterion 1, Audience, addresses the level of expertise expected of people who
will use the requirements. Do they need, for example, to have received formal
methods training? Or are the requirements intended for use by any stakeholder?

Criterion 2, Level of Abstraction (abbreviated in the assessment sections as
“Abstraction”), addresses the level of detail (of properties of the system
under description) which the requirements may or must cover.

Criterion 3, Associated method (“Method”), assesses whether the approach
includes a comprehensive methodology to guide the requirements process (as
opposed to more method-neutral approaches, which provide requirements support
but adapt to their users’ preferred methods).

Criterion 4, Tool Support (“Tools”), covers the availability of tools to
support the approach, as opposed to approaches that are conceptual only.

Criterion 5, Traceability support (“Traceability”), assesses how the approach
handles one of the most important issues associated with requirements: keeping
track of one- or two-way relations between requirement elements and their
counterparts in design, code and other project artifacts. The IEEE standards
emphasize the role of traceability as one of the key factors of requirements
quality.

Criterion 6, Non-functional requirements (“Coverage”), addresses whether the
approach covers only the description of functional properties of the system
(the functions it must perform, and environment constraints on these
functions) or extends to non-functional properties (affecting aspects other
than the system’s function, such as performance and security).

Criterion 7, Environment vs System (“Scope”), refers to the classic Jackson-
Zave distinction (Zave and Jackson, 1997) between two complementary parts of
the requirements: describing the environment (or ”domain”) in which the future
system will operate, and the constraints it imposes, such as “no car will
travel faster than 250 km/hour” or “any bank transfer above EUR 10,000 must be
reported”; and the system (or “machine”) which the project will build. Does
the approach cover both, or only the system part?

Criterion 8, Verifiability, assesses whether an approach supports the
possibility of formally verifying properties of the resulting requirements.
For approaches that provide such facilities, “formal verification” typically
means mathematical proofs, preferably supported by tools since manual
verification is not sufficient for large and complex systems.

Criterion 9, Semantic definition (“Semantics”), assesses the availability and
scope of a precise (if possible, formal) definition of the approach.

##  4\. Review of important approaches

We now explore the approaches in the order of the five categories of the
previous section, illustrating them through the example introduced in section
2 and evaluating them per the criteria of section 3.3.

###  4.1. Natural language

Natural language is, as noted, the dominant form of the requirements of
practical projects in industry. A number of requirements approaches
consequently start from natural language statements of requirements. Such
approaches face a fundamental challenge: software construction needs a high
degree of precision, but natural language is notoriously imprecise. ((Meyer,
1985) is a detailed analysis of the problems of using natural language for
requirements.) There are two ways of addressing these problems in practice:

  * •

Analyze the natural-language requirements texts, performing Natural Language
Processing (“NLP”) to extract precise information and in particular to detect
possible inconsistencies. Examples of methods using this approach include NL
to OCL (Hähnle et al., 2002), NL to STD and NL to OWL.

  * •

Constrain the kind of natural language used in requirements to ensure some
degree of precision, without going as far as the semi-formal and formal
approaches studied next. Examples include Requirements Grammar (4.1.1), Relax
(section 4.1.2) and Stimulus (section 4.1.3).

####  4.1.1. Requirements Grammar

Significant effort has been devoted to processing natural-language
requirements automatically, with the purpose of detecting inconsistencies and,
more generally, improving quality. Examples of such work include (Mich, 1996),
from 1996, and, more recently, (Slankas and Williams, 2013). Full natural-
language processing raises challenges at the frontier of artificial
intelligence research. To make the task more tractable, the Requirements
Grammar approach defines a structured, context-free subset of natural
language. Then the idea is that requirements elicitation will produce
requirements in this language, making it possible to avoid inconsistencies. As
with a programming language, the overall structure involves fixed keywords,
borrowed here from English, such as if and shall, but they can be combined
with free-form elements with no predefined meeting, as in

if the gears are locked down, the doors shall be closed

Fig. 1 shows a representation of requirements R11bis (_When the command line
is working, if the landing gear command handle has been pushed DOWN and stays
DOWN, then eventually the gears will be locked down and the doors will be seen
closed._) in this approach. The boxes shows the hierarchical structure.

Figure 1. Representation of requirement R11bis in Scott and Cook’s
Requirements Grammar

The grammar is not able to express this requirement as stated in section 2:
each requirement can only involve one _Independent Clause_ , with a single
_Subject of interest_. In the given requirement, there are two subjects (the
_gears_ and the _doors_). A solution is to split this requirement into two:

  * •

When the command line is working, if the landing gear command handle has been
pushed DOWN and stays DOWN, then eventually the gears will be locked down.

  * •

When the command line is working, if the gears are locked down, then
eventually the doors will be seen closed.

Then we adapt the result to the grammar according to the following scheme,
where keywords of the grammar appear in boldface:

Requirement::

a sentence corresponding to a requirement.

Independent Clause::

the mandatory part of the requirement, that describe the need,

Subject::

the subject of interest of the requirement,

shall::

a keyword,

Verb::

the action of the requirement,

Adjective:

or Noun Phrase: depending of the verb, a complement for the verb.

Temporal Conditional Clause::

an optional constraint on the requirement.

If::

a keyword,

Noun Phrase::

the subject of the constraint,

Verb::

the action of the constraint,

Adjective:

or Noun Phrase: depending of the verb, a complement for the verb.

Assessing Requirements Grammar according to the criteria of section 3.3:

  * •

Audience: since the notation, while constrained, uses a subset of natural
language, requirements are readable by any stakeholder, including those who
are not aware of the constraints and will only see a natural-language
description, possibly a bit contrived.

  * •

Abstraction: this approach is for requirements only, not influenced by
implementation concerns.

  * •

Method: the approach does not assume a particular requirements engineering
method.

  * •

Tool: the authors proposed a tool, named Badger111The tool seems no longer to
be available., to express requirements and analyze their lexical clauses.

  * •

Traceability: the approach focuses on requirements, independently of other
steps and products (design, implementation), so it offers no specific support
for traceability.

  * •

Coverage: given that the approach expresses requirements in a very abstract
form, it can include both functional and non-functional requirements.

  * •

Scope: the approach can cover both system and environment aspects.

  * •

Verification is limited to the following properties: consistency (the lexical
clause are analyzed to detect if all requirements follow the pattern).

  * •

Semantics: the syntax of specifications is defined precisely (through the
concept of context-free Requirements Grammar) but there is no corresponding
rigorous definition of the semantics.

####  4.1.2. Relax

Relax (Whittle et al., 2009) is a language for formal modeling of requirements
of CAS (Complex Adaptive System). The Relax syntax is close to natural
language. Fig. 2 shows requirements R11bis, R12bis, R21 and R22 expressed in
it.

R11bis::

The gear SHALL be locked down and the doors SHALL be closed AS EARLY AS
POSSIBLE AFTER the landing gear command handle has been pushed down and stays
down.

R12bis::

The gear SHALL be locked retracted and the doors SHALL be closed AS EARLY AS
POSSIBLE AFTER the landing gear command handle has been pushed up and stays
up.

R21::

The retraction sequence SHALL not be observed AS EARLY AS POSSIBLE AFTER the
command handle remains in down position.

R22::

The outgoing sequence SHALL not be observed AS EARLY AS POSSIBLE AFTER the
command handle remains in up position.

Figure 2. Representation of Landing Gear System requirements expressed with
Relax

Keywords such as AS EARLY AS POSSIBLE or AFTER express temporality of events.
They are semantically defined through a fuzzy branching temporal logic (FBTL)
(Moon et al., 2004), making it possible to submit the requirements to
validation tools. For example, R11bis can be translated into FBTL as:

$AG(A\mathcal{X}_{>(landing\\_gear\\_command=down)_{d_{2}}}(A\mathcal{X}_{\geq
d_{1}}(AG(gear=locked\\_down)\wedge AG(doors=closed))))$

(“In any state after the event ’landing gear command as been locked down’,
’gear is locked down and doors are closed’ becomes true in a near future
state.”) The example illustrates support for “fuzzy” notions (the F in FTBL)
such as “near”.

Relax places a particular emphasis on the expression of environment
properties. One can express such properties directly through the keyword
`ENV`, define “monitors” through `MON`, and express relationships between them
through `REL`.

An original feature of Relax, explaining the name, is the ability to mark some
requirements as critical, and to relax a non-critical requirement if necessary
to preserve the critical ones.

Assessing Relax according to the criteria of section 3.3:

  * •

Audience: the notation uses natural language expressions, requirements are
hence readable by any stakeholder.

  * •

Abstraction: this approach is for requirements only, not influenced by
implementation concerns.

  * •

Method: the approach does not assume a particular requirements engineering
method.

  * •

Tool: only propotypes such as Xtext (Eysholdt and Behrens, 2010) editors have
been developed around Relax.

  * •

Traceability: Relax focuses on requirements, independently of other steps and
products (design, implementation), so it offers no specific support for
traceability. Nevertheless the language provides a way to express
relationships between requirements (through the keyword `DEP`).

  * •

Coverage: targeting adaptive systems, Relax mainly addresses functional
requirements.

  * •

Scope: the approach explicitly covers system and environment aspects.

  * •

Verification is linked to the fuzzy branching temporal logic capabilities.

  * •

Semantics: on the basis of a precisely defined syntax for specifications,the
semantics is defined through FTBL (fuzzy branching temporal logic).

####  4.1.3. Stimulus

The Argosim Stimulus tool (Stimulus, 2015) expresses requirements in a
natural-language-like syntax (Jeannet and Gaucher, 2015), similar to Relax. It
is directed at stakeholders involved in system development.

Fig. 3 shows an initial attempt at expressing requirements _R11bis_ and
_R12bis_. It actually applies to a more complete version of the LGS example,
taking into account timing properties from the original LGS paper not included
above: a 15-second duration for retraction and for the outgoing sequence.

Figure 3. A possible representation of requirements R11bis and R12bis in
Stimulus

The idea is that after writing such an initial version one may, by simulating
inputs and observing outputs, detect possible problems and improve the
description. For example, Stimulus defines the semantic of _When_ as “ _at the
time the condition holds”_. Then _R11bis_ as defined in Fig. 3 (requirement
_[LS_RQ_001]_) uses both a _When_ and a _Do … afterwards_. Without this
clause, the _When_ would mean that When the handle is down, within 15 seconds
the doors shall be closed and the gears down, leaving the behavior undefined
afterwards. With the _Do … afterwards_ , the meaning is that after the handle
has been pushed down, within 15 seconds the doors shall be closed and the
gears down, remaining so until a new event.

Such wrong behavior can be detected through the Stimulus model-checker, which
simulates the system behavior by varying inputs. Users can observe the system
reaction and correct the requirements as needed. Stimulus favors such a
process of incremental improvement of the requirements.

Assessing Stimulus according to the criteria of section 3.3:

  * •

Audience: the language is close to natural language; requirements are readable
by any stakeholder.

  * •

Abstraction: this approach is for requirements only, not influenced by
implementation concerns.

  * •

Method: the approach does not assume a particular requirements engineering
method.

  * •

Tool: Stimulus is the name of both the language and the tool supporting it.

  * •

Traceability: the approach focuses on requirements, independently of other
steps and products (design, implementation), so it offers no specific support
for traceability.

  * •

Coverage: the approach covers only functional requirements.

  * •

Scope: the approach explicitly covers both system and environment aspects.

  * •

Verification can use model-checking to simulate a system’s reaction to various
inputs.

  * •

Semantics: The language is inspired by Lucid Synchrone (Colaço et al., 2005)
and Lutin (Raymond et al., 2008), defined in the literature with precise
semantics.

#### 4.1.A NL to OCL

(Hähnle et al., 2002) introduced a syntax to express constrained natural
language specifications. The tool is based on UML ((OMG), 2015) and the
associated OCL language ((OMG), 2014), a Design-by-Contract-like mechanism for
expressing semantic constraints on systems modeled in UML. It formalizes
constraints, originally expressed in constrained natural language, into OCL
(Object Constraint Language). The long-term goal is integration into the KeY
Java-oriented formal verification project (Ahrendt et al., 2005). The
presentation of NL to OCL described a tool for object-oriented modeling,
intended to allow non-experts to write constraints without having to embrace
full-fledged formal methods.

Operation:

retract

OCL::

context LGS::retract() pre: self.handle = up post: self.doors = closed and
self.gears = up

English::

for the operation retract() of the class LGS, the following precondition
should hold:
the handle is up
and the following post-conditions should hold:
the doors are closed the gears are up.

Figure 4. Fig. 1.A Possible representation of requirement R12bis with the NL
to OCL approach

Fig. 1.A expresses requirement R12bis using the NL to OCL approach. This
example (not tried out since the tool is no longer available) shows how to
match an English specification of the retract operation, including
precondition and postcondition, with its representation in OCL.

Assessing tNL to OCL according to the criteria of section 3.3:

  * •

Audience: the target users of OCL are software engineers able to read a UML
diagram and possessing a basic understanding of logic and formal reasoning.

  * •

Method: the implied methodology starts from constrained natural-language
requirements and expresses them in UML, with OCL for expressing semantic
properties.

  * •

Tool: the original tool for translation to OCL (Hähnle et al., 2002) is no
longer available. The UML part of the approach is supported by the wide range
of available UML tools (including other approaches for verification such as
(Cabot et al., 2007)).

  * •

Traceability: the requirements are expressed as contracts on operations,
linking them to the UML specification. There is, however, no specific support
for traceability to software artifacts.

  * •

Coverage: the approach applies to requirements whose semantics can be
expressed through contracts.

  * •

Scope: the approach only covers system aspects.

  * •

Verification: the idea is to use the KeY tool to verify consistency of
requirements.

  * •

Semantics: the OCL representation of requirements provides a semantic
definition.

#### 4.1.B NL to STD

The methodology of (Aceituna et al., 2011) iteratively transforms natural-
language requirements into State Transition Diagrams, defined as sets triples
[initial state, transition, resulting state].

Figure 5. Fig. 1.B Transformation from NL requirements to STD

Fig. 1.B illustrates the transformation of requirements into transition
diagrams. The first step {1} transforms requirements into diagram fragments.
For example, the requirement R11bis yields a transition from an unknown state,
when the handle is down, to a final state Gears locked down and doors closed.
Such states will have to be refined later. Step {2} assembles these fragment
into a single diagram, representing the entire system but not final since it
may still contain unknown states. Step {2} adds missing information and
repeats the process.

Assessing the NL to STD approach according to the criteria of section 3.3:

  * •

Audience: the requirements are first expressed in natural language, readable
by all stakeholders. The transition diagrams resulting from the transformation
in step 2 are meant for a more expert audience, but they include natural-
language explanations coming from the original text.

  * •

Abstraction: this approach is for requirements only, not influenced by
implementation concerns.

  * •

Method: the approach proposes a method as outlined (going from natural
language to transition diagrams).

  * •

Tools: the translation into transition diagrams is manual.

  * •

Traceability: there is no specific support for traceability.

  * •

Coverage: given that the approach expresses requirements in a very abstract
form, it can include both functional and non-functional requirements.

  * •

Scope: the approach can cover both system and environment aspects.

  * •

Verification: transition diagrams are formal texts, which can be submitted to
tools.

  * •

Semantics: State Transition Diagrams are a well-known notion with precise
semantics.

####  4.1.4. NL to OWL

The approach of (Li et al., 2015) translates natural-language requirements
into an intermediate requirements modeling language that can be easily
formalized in OWL (Bechhofer, 2009).

In the example, requirement R11bis – _When the command line is working, if the
landing gear command handle has been pushed down and stays down, then
eventually the gears will be locked down and the doors will be seen closed_ –
yields two functional goals:

> FG11-1 := lock_down $<$object: {the gears}$>$ :$<$ $<$trigger: push_down
> $<$object: {landing gear command handle}$>$$>$
> FG11-2 := close $<$object: {the doors}$>$ :$<$ $<$trigger: FG11-1$>$$>$

FG11-1 states that the gears should be locked down a while after the landing
gear command handle has been pushed down. FG11-2 states the obligation to
close the doors when the gears are locked down, as triggered by the first
functional goal. R12bis can be modeled in a similar way.

The requirement R21 – _When the command line is working, if the landing gear
command handle remains in the down position, then retraction sequence is not
observed_ – can be modeled using only one functional goal:

> FG5 := extend $<$object: {the gears}$>$ :$<$ $<$trigger: remains_down
> $<$object: {landing gear command handle}$>$$>$

This functional goal models the need to do not observe retraction sequence –
and so, extend the landing gears – when the handle remains down. Requirement
R22 can be modeled in a similar way.

Assessing NL to OWL according to the criteria of section 3.3:

  * •

Audience: requirements engineers.

  * •

Abstraction: requirements only, no tainting by implementation.

  * •

Method: NL to OWL guides the requirements process, from natural language to
more formal.

  * •

Tool: none directly for the method; there are tools for OWL such as Protégé
(Protégé, 2016).

  * •

Traceability: requirements are decomposed into ontologies, sharing the same
namespace, which can be used to create links between several requirements.

  * •

Coverage: both functional (_functional goals_) and non-functional properties
(_quality goals_).

  * •

Scope: both system and environment (represented through _domain assumptions_).

  * •

Verification: no support for requirements verification of (though OWL has a
formal semantics).

  * •

Semantics: from OWL.

###  4.2. Semi-formal

A number of approaches, including both research efforts and industrial
products, use partially formalized notations. Some of the most important,
reviewed below, are Doors, Reqtify, KAOS and SysML, as well as (in the full
version only) URN and URML.

####  4.2.1. Doors and Reqtify

Doors (IBM, 2015) and Reqtify (Systems, 2016) are widely used in industry.
They are semi-formal in the sense that they require a partially structured
approach to requirements management. While they are distinct products from
different providers (respectively IBM Rational and Dassault Systems), they are
often used jointly and we cover them together. In both cases the focus is not
on producing requirements, but on managing requirements independently of how
they were produced.

Doors is a collaborative tool allowing different stakeholders to work on
requirements, typically maintained as spreadsheets, and set priorities
according to levels of risks. Reqtify’s focus is on traceability: the tool
supports defining relationships between requirements typically expressed in
natural language and coming from such tools as Microsoft Word, spreadsheets or
modeling tools.

Since these approaches do not define any specific method or notation for
expressing requirements, we cannot demonstrate them on the running case study.
In the operational practice the requirements would be expressed in some
document, e.g. Word or PDF. DOORS would then record this document and its
various attributes (creation date, version number, priority…) in its database,
supporting the management of these requirements throughout the project.
Reqtify would support defining and managing a traceability between their
various elements.

With respect to the criteria of section 2:

  * •

Audience: aimed at a large audience of stakeholders, no particular technical
prerequisite.

  * •

Abstraction: focused on requirements no influence from implementation.

  * •

Method: these are software tools, with no particular method attached.

  * •

Traceability: traceability is the strong point of Reqtify in particular, which
offers support for tracing requirements from specification to design and code.
For example, it makes it possible to import requirements expressed in a
Microsoft Word document and link them to C code.

  * •

Coverage: no particular restriction of coverage or scope.

  * •

Semantics: nor formal semantics, no verification methodology.

####  4.2.2. KAOS

KAOS (Dardenne et al., 1993), like i* ((Yu, 1997)), is based on the Goal-
Oriented Requirements Engineering approach to requirements (van Lamsweerde,
2001) (van Lamsweerde, 2004) (Yu and Mylopoulos, 1998). The key idea of this
approach is to base requirements on a higher-level concept, goals. A goal is
statement of intent expressed in terms of business needs (such as “turn more
sales inquiries into actual sales” for a customer management sytem).
Requirements then express system properties helping to achieve these goals.
(Specifically, R, A, D $\models$ G with sets of requirements R, domain
assumptions A, domain properties D and goals G.) Goals can be composite,
expressed in terms of simpler goals through trees operators including AND, OR
and “+” (denoting a less formal relation, “contributes to”). The general
approach is refinement-based: start from high-level goals and decompose them
using the operators. A non-composite goal is called a “requisite”. The OR
operator makes it possible to include alternative paths.

KAOS uses natural language to express goals and a semi-formal notation for
relationships between goals, with concepts such as “milestone” and “
conflict”, and supports the refinement process.

Goals cover both system and environment properties: if a requisite can be
assigned to an agent of the system, it is an “operational goal”, describing a
system property. Otherwise it is an “expectation”, describing an environment
property.

Figure 6. Excerpt of the KAOS diagram of requirements R11 bis and R21 of the
LGS (Objectiver)

The LGS model of Fig. 6 covers entities including door, gear and handle. Both
R11bis and R21 refine the goal «When handle is down, gears are extended and
doors are closed», which assumes normal mode and is itself part of the
refinement of a more global goal defining the whole system’s safety. «Outgoing
operation» addresses R11bis and R21 by managing the LGS outgoing sequence:
after an the LG command, the handle has been moved up, doors remain closed and
gears locked down. Some agent, triggered by the event “handle pushed down”,
will be responsible for this operation.

Assessing KAOS according to the criteria of section 2:

  * •

Audience: KAOS requires modeling experience, and some training in the method.

  * •

Abstraction: no influence from implementation. KAOS can in fact be described
as particularly abstract since it focuses on a concept, goals, which is even
higher than requirements.

  * •

Method: KAOS includes a general methodology for modeling systems, specifying
dependencies between requirements, and refining goals.

  * •

Tool: Objectiver (Respect-it, 2011) supports the expression and refinement of
user requirementsin KAOS.

  * •

Traceability: there is support for linking to specification documents.

  * •

Coverage: mostly functional requirements, but can include some non-functional
ones.

  * •

Scope: both system and environment through the notion of operational goal and
expectation in the refinement process, as described above.

  * •

Verification: no specific support (graphical notation).

  * •

Semantics: behavioral goals can be described in temporal logic (LTL) or in
event-B ((Abrial, 2010)) (Matoussi et al., 2010).

#### 4.2.A. URN

User Requirements Notation (Amyot, 2003) is a recommendation of the
International Telecommunication Union (standard Z.151, from 2008, updated
2012, third version in progress) for the modelling, analysis, specification
and validation of requirements, used mainly for business process modeling.

The basic concepts are goals, scenarios, and links between such elements. URN
combines two complementary views: static goals, through the Goal-oriented
Requirement Language (GRL); and dynamic scenarios, through the Use Case Map
(UCM) notation. Both notations support checking: for GRL models, through
“strategies”, representing initial situations; for UCM models, through
“scenarios”, similar to test cases. There is also a framework for formal
verification of UCM ((Hassine, 2010), including time extensions. For
traceability:

  * •

Internally: URN supports links connecting GRL and UCM models, enabling
completeness and consistency analysis.

  * •

With external notations: through such tools as jUCMNav (Jucmnav), to integrate
URN models with DOORS.

For verification, methodological elements support validating goal-oriented
models and resolving conflicts ((Hassine and Amyot, 2016) (Hassine and Amyot,
2017)).

Figure 2.A uses GRL to describe the goals of the LGS example. The overall goal
LGS Safe is decomposed into two goals (among others), reflecting R21 and R22
and refined further into more specific goals reflecting R11bis and R12bis. A
task contributes to a goal: the “outgoing” task contributes to R11bis and
“retracting” to R12bis. Note that tasks may depend on resources (that is not
the case here).

Figure 7. Fig. 2.A Partial URN diagram for LGS requirements R11 bis and R21
(jUCMNav)

Assessing URN according to the criteria of section 2:

  * •

Audience: URN needs a specific training on GRL and UCM.

  * •

Abstraction: the approach does not have implementation concerns

  * •

Method: URN does not impose any development process, but tutorials about
jUCMnav present methodological elements.

  * •

Tools: jUCMNav is the open-source Eclipse (foundation, 2004) plugin that
supports URN ((Roy et al., 2006)). Others include OpenOME (OpenOme, 2000)
Sandrila (Sandrila, 2019) UniqueSoft (UniqueSoft, 2020) ArchSync (ArchSync,
2006) and TouchCORE (TouchCORE, 2020)

  * •

Traceability: as noted, URN support links between model elements.

  * •

Coverage: GRL focuses on requirements, especially non-functional ones. UCM is
most useful for specifying functional requirements.

  * •

Scope: URN is dedicated to systems and specifically to reactive systems and
business systems.

  * •

Verification: no formal support (beyond the methodological elements mentioned
above).

  * •

Semantics: from (Amyot and Mussbacher, 2011), “the URN standard describes the
URN abstract and concrete syntaxes formally, together with well- formedness
constraints. However, the semantics is currently described more informally”.

####  4.2.3. SysML (Systems Modeling Language)

SYStem Modelling Language ((OMG), 2007) is an extension of UML ((OMG), 2015)
dedicated to systems engineering. SysML provides requirements diagrams, which
allow users to express requirements in textual representation, and cover non-
functional requirements. The requirements diagram of SysML provides ways to
express traceability links between different requirements (containment,
derive, copy, trace) or between requirements and implementation elements
(satisfy, verify, refine). Relationships between requirements and other
modeling artifacts (like blocks, use cases, activities, …), allow basic
verification (e.g. each requirement is supported by at least one modeling
element, …). A formal expression of requirements and thus their formal
verification is not possible. The SysML requirements diagram of Fig. 8
expresses the links between the LGS requirements R11bis to R22 and the landing
gear block.

Figure 8. Exerpt of the SysML functional requirements diagram of LGS (Papyrus)

Assessing SysML according to the criteria of section 2:

  * •

Audience: SysML is a modeling language needing specifc knowledge.

  * •

Abstraction: SysMl stands at a high level of abstraction. Its requirement
diagram enables quick requirements analysis and visual design.

  * •

Method: SysML, like UML, is a notation, providing no methodology.

  * •

Tool: It is supported by a number of tools such as IBM Rhapsody (IBM, 2016),
Modelio (ModelioSoft, 2017), Enterprise Architect (Systems, 2017), Papyrus
(foundation, 2015), …that implement a methodology preconised for using SysML.

  * •

Traceability: SysML provides traceability links.

  * •

Coverage: SysML supports both functional and non-functional requirements.

  * •

Scope: SysML focuses on system requirements, particularly for complex systems.

  * •

Verification: SysML does not allow any verification.

  * •

Semantics: SysML does not provide any semantic definition of the approach.

#### 4.2.B. URML

User Requirements Modeling Language (Helming et al., 2010; Berenbach et al.,
2012) is a UML profile developed in collaboration between the Technical
University of Munich and Siemens. The approach unifies concepts from goal-
oriented, feature-oriented, process-oriented, and risk-oriented approaches,
integrating them into models covering both functional and nonfunctional
requirements.

RML is a language in its own right, based on the “Meta-Object Facility” (MOF),
with a meta-model mapped to a UML profile to implement the supporting tools.
As a consequence, URML provides a graphical, icon-based notation to express
requirements as well as associated notions such as threats, hazards,
mitigations and even product lines and stakeholders.

It is possible to associate semantic properties — such as presupposes,
details, constrains, refines, with, … — with URML links between requirements
and other artifacts.

The modeling focus is on systems, but URML can also describe properties of the
environment.

URML is more particularly dedicated to requirements elicitation, and does not
provide any specific methodology to construct models, but it can support any
methodology compatible with the URML meta-model.

Figure 2.B is an excerpt of a URML model of the LGS. To ensure a basic
functionality of the LGS and its safety, we need to consider the outgoing
sequence of the gears. This process is supposed to achieve the goal “when the
LG command is down, gears are extended and doors are closed”. To do so, it
requires both R21 and R11bis. R11bis is considered a refinement of R21 since
it expresses the same need at a finer level of detail.

Figure 9. Fig. 2.B Excerpt of the URML requirements diagram of LGS (Enterprise
Architect)

Assessing URML according to the criteria of section 2:

  * •

Audience: as URML is an icon-based graphical modeling language, the learning
process of abstractions of this requirements language will be easy.

  * •

Abstraction: URML is based on abstractions of requirements.

  * •

Method: this approach does not assume a particular requirements engineering
method

  * •

Tool: it is supported by an Enterprise Architect Add-On. (Systems, 2017).

  * •

Traceability: the links between concepts can lead to traceability.

  * •

Coverage: URML integrates functional and nonfunctional requirements.

  * •

Scope: it is focused on systems and particularly complex systems

  * •

Verification: no mean is provided to do verification of requirements.

  * •

Semantics: some semantics can be put on links between requirements and other
artifacts.

###  4.3. Graphs and automata

A number of approaches rely on the mathematical theories of graphs and
automata, well known in computer science (Minsky, 1967) and supported by
effective graphical representations.

Such approaches are often used to represent the dynamic aspects of a system,
particularly behavior and timing. We examine Petri nets, Statecharts, Problem
Frames, FSP/LTSA, and FORM-L. Other approaches offering different flavors of
the same concepts include UML Activity Diagrams and State Diagrams (OMG,
2011), UPPAAL (Pettersson and Larsen, 2000), DEVS (Cellier, 1991) and SCXML
(State Chart XML (SCXML), 2012).

#### 4.3.A Petri Nets

A Petri net (Peterson, 1977) is a directed graph, where each node is either a
place (circle, representing a condition) or a transition (bar) and each edge
is associated with a transition. An example appears in Figure 3.A.

Petri nets have been known for several decades and have been used for many
applications, Their attractiveness comes from the simplicity of the model and
its ability to describe processes in a clear, visual way with a precise
mathematical basis. They suffer, however, from a lack of compositionality
making them unsuitable, in the view of critics, for scaling up to the
description of large systems. A good analysis of the pros and cons can be
found in(Zurawski and Zhou, 1994).

Figure 10. Fig. 3.A Petri Net model of an Electrical Circuit of Negative
Pressuring Electro-valve (taken from (Villani et al., 2004))

Assessing Petri nets according to the criteria of section 3.3:

  * •

Audience: the notation, while graphical and clear, has to be learned.

  * •

Abstraction: this approach is for requirements only, not influenced by
implementation concerns.

  * •

Method: the approach does not assume a particular requirements engineering
method.

  * •

Tool: Petri nets have been around for a long time; many tools have been
developed to edit, execute and verify nets.

  * •

Traceability: the approach focuses on the expression of dynamic behavior
requirements, and offers no specific support for traceability.

  * •

Coverage: Petri nets in their basic form address functional requirements.

  * •

Scope: Petri nets only cover the modeling of the precise behavior of some
parts of the system rather than the environment. Is is hence limited to fully
express requirements of a system.

  * •

Verification is supported by Petri-net tools, relying on model-checking.

  * •

Semantics: Petri nets have an exact mathematical definition of their execution
semantics, with a well-developed mathematical theory for process analysis.

####  4.3.1. Finite automata, state diagrams and statecharts

The most widely used kind of automaton, notable for the simplicity and power
of the concept, is the finite automaton, used (in applications to system
modeling) through the closely related mechanism of a finite-state diagram.
Such a diagram is a mathematical device defined by a finite set of states,
each representing a possible configuration of a system or computation, the
designation of some of the states as initial and some as final, and a finite
set of transitions between states. Each transition models the effect of a
given event in a certain state, by defining the resulting state or states. To
model an entire system execution, the automaton starts in an initial state
then processes events by following the corresponding transitions until it
reaches a final state.

Part of the attraction of finite-state diagrams is that they enjoy a natural
representation as graphs, with nodes as states and transitions as edges, as
illustrated in Fig. 11.

Figure 11. A finite-state diagram for the LGS Door

The most widely used finite-state diagram notation for describing the behavior
of systems is the Statechart (Harel, 1987) or “Harel chart”. A system is
described through a finite number of states and transitions between those
states (see Fig. 11). Statecharts enjoy a well-documented formal definition
and are suitable for the modeling of parallel systems.

Assessing Statecharts according to the criteria of section 3.3:

  * •

Audience: the notation, while graphical, assumes an understanding of the
semantics.

  * •

Abstraction: Statecharts are meant for specification, independently of
implementation concerns, and is abstract due to its specific notation. Note
that available tools provide an execution environment to animate state
machines (for simulation rather than actual implementation).

  * •

Method: the approach enforces a strong methodological discipline, based on
modeling systems in the form of states and transitions.

  * •

Tool: many tools and languages are using Statecharts principles, sometimes
redefining some of the semantics (e.g., UML).

  * •

Traceability: the approach focuses on the expression of dynamic behavior
requirements and offers no specific support for traceability.

  * •

Coverage: Statecharts mainly address functional requirements.

  * •

Scope: there is no specific modeling of the environment, although events
leading to transitions can come from the outside or the inside of the system.

  * •

Verification: supported by the semantics implementation of the tools, using
model-checking.

  * •

Semantics: the basic semantics of Statecharts comes from the theory of finite-
state automata.

####  4.3.2. Problem Frames

(Jackson, 2001) is an approach to software requirements analysis developed by
Michael Jackson in the nineties. It has influenced number of subsequent
approaches because it brought to light the need to divide requirements into
system and environment properties. As defined by M. Jackson, a problem frame
“defines the shape of a problem by capturing the characteristics and
interconnections of the parts of the world it is concerned with, and the
concerns and difficulties that are likely to arise.” Problem Frames provide a
methodology for decomposing requirements, treated as relationships between the
system and the real world. Fig. 12 depicts a problem diagram with a concrete
machine domain on the left (Computing Module), its corresponding domain in the
middle (Landing Set) and the requirement on the right that lead to this
domain. The Computing Module is the software control machine that controls the
Landing Set domain to ensure the behavioral requirement mentioned on the
right. By dividing a software purpose into a set of manageable and well
documented pieces it is easier to apprehend a complex problem. In addition
this decomposition makes the pieces easier to reuse in the sense that when
reused, one can benefit from the exact context (domain and requirement) of
this particular piece of software.

Figure 12. LGS Landing Set Problem Diagram

The Problem Frames approach is important for its historical influence on other
approaches and its clear distinction between system and environment. Assessing
it accor ding to the criteria of section 3.3:

  * •

Audience: The notation, while graphical and intuitive, is very specific and is
targeted to Problem Frames specialists only.

  * •

Abstraction: this approach is for requirements mostly, not influenced by
implementation concerns, and is very abstract due to its specific notation.

  * •

Method: the approach is strongly related to Jackson’s methodology but has no
particular traceability nor non-functional requirements support.

  * •

Tool: the approach provides a set of notations, some of them graphical such as
context diagrams or problem diagrams (see Fig. 12).

  * •

Traceability: the approach focuses on the expression of dynamic behavior
requirements and offers no specific support for traceability.

  * •

Coverage: Problem Frames mainly address functional requirements.

  * •

Scope: Problem Frames focus on the modeling of the system in its environment,
treating both aspects as equally important.

  * •

Verification: the approach is not designed for verification.

  * •

Semantics: while precise, the graphical notation of Problem Frames has no
precise semantics.

####  4.3.3. FSP/LTSA

“Process algebras”, which provide a formal basis for describing interactions
between processes, have influenced several methods. The original process
algebras were Hoare’s CSP (Communicating Sequential Processes) (Hoare, 1978)
and Milner’s CCS (Communicating Sequential Processes), later extended to cover
mobile agents in the $\pi$-calculus (Milner, 1982). FSP (Finite State
Processes) proceeds from both CSP and CCS.

The basic unit of all process algebras is a concurrent process which can
communicate with others through input and output ports. For requirements,
communication can model interaction both within the system and with the
environment. Specifications in this style can formally express such essential
temporal properties as liveness, safety, progress and fairness, and use
supporting tools to verify them.

For FSP the supporting tool is LTSA (Labeled Transition System Analyzer (Magee
and Kramer, 1999)). From an FSP model, LTSA generates a Labeled Transition
System (LTS), suitable for automated analysis and animation. LTSA is
compositional, meaning that it is possible to model the components of a system
separately then, with process calculus mechanisms, their composition. In
addition to helping the modeling process, LTSA’s compositionality benefits the
verification process: one may verify safety and liveness properties by model-
checking individual components then their composition.

FSP can take advantage of compositionality to model the LGS example as the
parallel composition (expressed through the `||` operator) of two distinct
processes:

    ||LGS = (LGS_BEHAVIOR || CONTROL_HANDLE)

CONTROL_HANDLE specifies how the state of the handle may change, and
LGS_BEHAVIOR how the LGS reacts to these changes.

The history of a process’s execution, called a trace, is defined by a sequence
of transitions each executed in response to a certain event from the alphabet
of the process. Processes such as the above two interact through events in the
intersection of their alphabets, such as “up” and “down”.

The concept of fluent serves to express that a process may be in a certain
state which it can only leave through specific transitions. For example,
specifying

    fluent HANDLE_IS_DOWN = <{down}, {up}>
    fluent HANDLE_IS_UP = <{up}, {down}>

specifies the notion of the handle staying up and down in “the handle has been
pushed up and stays up”, from requirements R12bis and R22, and the dual
property from R11bis and R21. Only the specified transitions can, in each
case, set and unset the fluent.

Here are further fluents for LGS, some with more than one setting or resetting
event:

    fluent DOOR_IS_CLOSING = <{start_closing}, {end_closing, open}>
    fluent DOOR_IS_CLOSED = <{end_closing}, {open}>
    fluent GEAR_IS_EXTENDING = <{start_extension}, {end_extension, start_retraction}>
    fluent GEAR_IS_EXTENDED = <{end_extension}, {start_retraction}>
    fluent GEAR_IS_RETRACTING = <{start_retraction}, {end_retraction, start_extension}>
    fluent GEAR_IS_RETRACTED = <{end_retraction}, {start_extension}>

Some of the new events, such as start_closing, do not immediately reflect an
event expressed in the informal LGS specification, but are an artifact for
expressing timing properties in the FPS framework.

LTSA also supports assertions to express properties of the system. In the LGS
example:

    assert R21 = [] ([] HANDLE_IS_DOWN -> [] ! GEAR_IS_RETRACTING)
    assert R22 = [] ([] HANDLE_IS_UP -> [] ! GEAR_IS_EXTENDING)
    assert R11bis = [] ([] HANDLE_IS_DOWN -> <> [] (GEAR_IS_EXTENDED && DOOR_IS_CLOSED))
    assert R12bis = [] ([] HANDLE_IS_UP -> <> [] (GEAR_IS_RETRACTED && DOOR_IS_CLOSED))

with the following syntax for operators of boolean and temporal logic: ! is
negation, && is conjunction, -¿ is implication, [] is “always” and
$\langle\rangle$ is “eventually”.

The specification as given so far would not verify because of FPS’s default
assumption of equal priority of all applicable transitions,to ensure fairness.
In R21, [] HANDLE_IS_DOWN cannot hold because an “up” event will eventually
invalidate this fluent; similarly for R11bis. To resolve such situations, LTSA
provides the lower priority operator, written $\rangle\rangle$. We can use it
to resolve the conflict in favor of “down” by lowering the priority of “up”,
rewriting the definition of the system as

    ||LGS = (LGS_BEHAVIOR || CONTROL_HANDLE) >> {up}.

and use the following auxiliary assertion to check the effect:

    assert EVENTUALLY_ALWAYS_DOWN = <> [] HANDLE_IS_DOWN

Then R21 and R11bis will verify but not R22 and R12bis, for which we would
need instead to decrease the priority of “down” and assert
EVENTUALLY_ALWAYS_UP. It is a characteristic of LTSA that in such cases one
cannot verify both sets of assertions under the same conditions.

Appendix A contains the complete FSP model for the LGS example. The reader may
input it “as is” into the LTSA analyzer.

Appendix A contains the complete FSP model for the LGS example. An interested
reader may put it into the LTSA analyzer as it is to do some experimenting.

Assessing LTSA according to the criteria of section 3.3:

  * •

Audience: the FSP notation is mathematically formal and requires the
corresponding qualification both from the specifiers and the readers.

  * •

Abstraction: the FSP abstraction is suitable both for specifying systems’
implementations and for specifying requirements.

  * •

Method: the approach does not assume a particular requirements engineering
method.

  * •

Tool: the LTSA tool supports model-checking FSP specifications, execution of
specifications, and graphical simulation.

  * •

Traceability: the approach focuses on model-checking FSP specifications, so it
offers no specific support for traceability.

  * •

Coverage: LTSA can specify and model-check liveness, safety, progress and
fairness.

  * •

Scope: The approach can cover both system and environment aspects of
requirements.

  * •

Verification: LTSA supports verification of liveness, safety, progress, and
fairness properties.

  * •

Semantics: the FSP semantics is rigorously defined (Magee and Kramer, 1999).

####  4.3.4. FORM-L

FORM-L (Nguyen, 2015) extends MODELICA (Modelica, 2017), an object-oriented
notation for modeling the behavior of physical systems. FORM-L results from
the MODRIO project (MOdel DRIven physical systems Operation), which improved
MODELICA by adding the modeling of assumptions on the environment. Fig. 13
shows an example FORM-L specification.

Figure 13. Example of FORM-L requirement

FORM-L addresses the early stage of system development, with a level of detail
sufficient to support some early validation through model-checking using the
Stimulus tool (Stimulus, 2015). There is no particular method attached to
FORM-L, also no support for traceability and non-functional requirements.
Thanks to its formal semantics and to the support of a transformation (e.g.,
to , the FORM-L requirements can be verified by model-checking.

Assessing FORM-L according to the criteria of section 3.3:

  * •

Audience: the FORM-L notation is mathematically formal and requires the
corresponding qualification both from specifiers and readers.

  * •

Abstraction: the FORM-L abstraction is suitable both for specifying systems’
detailed design and for specifying goals and requirements.

  * •

Method: The approach does not assume any particular requirements engineering
method but the main definition steps focus on: Goals, Requirements,
Specification, Design.

  * •

Tool: Only tools internal to EDF, the organization that developed FORM-L,
support code generation and simulation.

  * •

Traceability is among the goals but with no supporting mechanisms so far.

  * •

Scope: the approach can cover all aspects of requirements, including both
system and environment aspects.

  * •

Verification: the approach supports simulation.

  * •

Semantics: the FORM-L notation is in the process of being formalized by
providing a formal semantics to a kernel set of FORM-L concepts.

###  4.4. Other mathematical frameworks

Requirements can use other mathematical theories other than graphs and
automata, for example set theory, the ultimate basis for the two approaches
discussed below, Event-B and Alloy. Other important mathematics-based
approaches include VDM (Vienna Development Method), FSP/LTSA and Tabular
Relations, both presented in the online version of this article.

####  4.4.1. Event-B

Event-B (Abrial, 2010) is a formal method for system-level modeling and
analysis. Modeling proceeds by specifying the system’s state in terms of sets
and functions, and specifying state transformation in terms of events. THe
mathematical basis is set theory complemented by refinement, a mechanism for
turning a description of a system at a certain level of detail into a new one
that remains consistent with it but includes more details. To ensure this
consistency, a refinement must preserve the invariants from the original
description, while possibly adding new ones. The preservation of invariants
must be proved mathematically, with the help of the supporting tools.

Three fragments of an Event-B model for the LGS will illustrate the ideas.
Fig. 14 shows an event modeling the extension of the gear. The Boolean
variable gear_extended_p expresses whether the gear is extended or not. Fig.
15 shows an event modeling the retraction of the gear. Another Boolean
variable, gear_retracted_p, models whether the gear is retracted or not. Fig.
16 shows an invariant stating that the gear cannot be extended and retracted
at the same time.

Figure 14. Event to model gear extension (edited from (Mammar and Laleau,
2017)) Figure 15. Event to model gear retraction (edited from (Mammar and
Laleau, 2017)) Figure 16. Invariant: a gear cannot be extended and retracted
at the same time (edited from (Mammar and Laleau, 2017))

Assessing Event-B according to the criteria of section 3.3:

  * •

Audience: The notation requires familiarity with classical set theory; while
the concepts are elementary, they exclude stakeholders who feel uncomfortable
with mathematics.

  * •

Abstraction: Through successive refinement, the approach covers the full
spectrum from very abstract and partial models to detailed final models ready
for translation into an implementation.

  * •

Method: beyond the notation, Event-B is a full-fledged method based on
successive refinements proved correct (invariant-preserving). The method does
not cover the entire process of requirements engineering (e.g. how to obtain
requirements from stakeholders), only the refinement and proof process.

  * •

Tool: tools support the refinement and proof process, particularly in the
Rodin environment (Event-b, 2018).

  * •

Traceability: this is not a particular focus of the Event-B method, although
it is possible to trace the identifiers used throughout the refinement
process.

  * •

Coverage: the approach makes it possible to model both a system and its
environment.

  * •

Scope: Event-B has no particular mechanism for modeling non-functional
requirements.

  * •

Verification: requirements expressed in Event-B are verifiable through the
proof process which accompanies refinement: the description at every step of
the refinement must be proved consistent with the description at the preceding
(immediately higher) level. As a consequence, Event-B has been successfully
used in several industrial projects requiring proofs of correctness, for
example in the transportation and aerospace fields, and in business management
(Romanovsky and Thomas, 2013). In combination with other requirements
approaches, such as Problem frames (Jackson, 2001), it has also been used in
the automotive industry (Gmehlich et al., 2013).

  * •

Semantics: the behavioral semantics of Event-B refinement has been described
in (Schneider et al., 2014).

#### 4.4.A Vienna Development Method

The Vienna Development Method (VDM) (Bjørner and Jones, 1978), originally
developed at the IBM Laboratory in Vienna in the 1970s, was one of the first
formal methods in the history of software and system modeling. It includes the
VDM Specification Language (VDM-SL) (Project, 2017) and its extended form
(VDM++) (Durr and van Katwijk, 1992). VDM-SL uses modules, while VDM++ applies
object-oriented structuring with classes and multiple inheritance. Computing
systems may be modeled in VDM-SL at a high level of abstraction, then
transformed into progressively more detailed designs through a refinement
process (reification) similar to the Event-B ideas.

VDM-SL allows users to express different states of the systems and invariants
that shall be met. As an example, Figure 4.A expresses requirements R21 and
R22.

[label=lst:vdm-state,title=Figure 4.A. VDM-SL representation of the LGS
states, with requirements R21 and R22] state LGS of gears: ¡retracted¿ —
¡extended¿ — ¡retracting¿ — ¡extending¿ doors: ¡opened¿ — ¡closed¿ — ¡opening¿
— ¡closing¿ handle: ¡down¿ — ¡up¿ inv mk_LGS(gears, doors, handle) == (handle
= ¡down¿ =¿ gears ¡¿ ¡retracted¿) and (handle = ¡up¿ =¿ gears ¡¿ ¡extended¿)
init lgs == lgs = mk_LGS(¡extended¿,¡closed¿,¡down¿) end

Another way to introduce requirements into a VDM specification is to translate
the requirements into pre- and post-conditions of operations. For example, the
requirement R11bis (resp. R12bis) is a description of what happens when handle
remains down (up). Figure 4.B specifies these operations; the pre clause
expresses the condition under which the operation may be called, and the post
clause characterizes the state after execution. [label=lst:vdm-
operations,title=Figure 4.B VDM-SL operations specified by requirements R11bis
and R12bis] operations extension_sequence() ext wr gears wr doors rd handle
pre handle = ¡down¿ post handle = ¡down¿ =¿ (gears = ¡extended¿ and doors =
¡closed¿);

retraction_sequence() ext wr gears wr doors rd handle pre handle = ¡up¿ post
handle = ¡up¿ =¿ (gears = ¡retracted¿ and doors = ¡closed¿); end LGS The rd
(read-only) and wr (read-write) clauses specify which parts of the LGS the
operations may access and modify.

Assessing VDM according to the criteria of section 3.3:

  * •

Audience: VDM requires an understanding of mathematical foundations.

  * •

Abstraction: VDM is a mathematical formalism, suitable for the early stages of
the development process.

  * •

Method: VDM supports the description of data and functionality. Data are
defined by means of types. Functionality is defined in terms of operations.

  * •

Tool: VDM is mature and has an extensive tool support (e.g.,
Overture(Overture, 2020)).

  * •

Traceability: VDM has no specific support for traceability.

  * •

Coverage: The approach covers the expression of requirements on both the
system and environment aspects.

  * •

Scope: VDM covers the functional part of requirements.

  * •

Verification: Supporting tools are available to verify VDM specifications.

  * •

Semantics: VDM has a formal semantics, published as an ISO (International
Standards Organization) standard.

#### 4.4.B Process Algebra

While Model-based formalisms such as Event-B and VDM are concerned with
functional properties and sequential behavior, process algebras are concerned
with interaction between concurrent processes. Among the original methods in
this field, we can mention CSP (Hoare, 1978) and CCS (Milner, 1982). Mobile
process algebras (e.g. Milner’s $\pi$-calculus (Milner, 1982)) represent a
further development by addressing channel mobility. The basic unit of all
process algebras is a communicating concurrent process with its own input and
output ports, which makes feasible modeling the interaction with the
environment and expressing requirements beyond the system itself.

Assessing Process Algebra according to the criteria of section 3.3:

  * •

Audience: the intended audience is that of specialist, mathematician and
software engineer with deep understanding of foundations.

  * •

Abstraction: Process Algebra can model a system at the level of abstraction of
processes, regardless of the internal operational logic.

  * •

Method: while Event-B is equipped with its own methodology base on refinement,
Process Algebras are mainly a notation, although coming with notions of
behavioral equivalence and techniques to formally prove processes semantical
equivalence.

  * •

Tool: the approach is not highly practical. Tool support is still limited:
TyPiCal is a type-based static analyzer for the $\pi$-calculus (Kobayashi, ).
TyPiCal is able to provide four different kinds of program analyses and
transformations: lock-freedom analysis (certain communications or
synchronizations will eventually succeed), deadlock-freedom analysis, useless-
code elimination (it removes sub-processes that do not affect the observable
behavior of the process), and information flow analysis.

  * •

Traceability: requirements traceability is not supported.

  * •

Coverage: among Process Algebra, CSP is possibly the one with the broadest set
of concrete applications, typically in protocol analysis (Lowe, 1996) or as a
model for construction of parallel programming languages (Hull, 1987). Mobile
Process Algebras such as the $\pi$-calculus have been instead mostly applied
to the definition and formalization of service orchestration languages (Lucchi
and Mazzara, 2007; Mazzara, 2006).

  * •

Scope: non-functional requirements are not expressible.

  * •

Verification: when both requirements and implementation are expressed in the
form of a process, behavioral equivalence could be used to verify consistency.

  * •

Semantics: all the algebras mentioned above come with their own formal
semantics, often expressed via Structured Operational semantics (SOS).

####  4.4.2. Alloy

Alloy (Jackson, 2006) is a declarative modeling language based on first-order
logic for expressing the behavior of software systems. It shares its roots
with Event-B, since Alloy is a subset of the Z set-theory-based specification
language (Abrial et al., 1980), which also served as the starting point for
Event-B.

Alloy has spurred a significant research community and a number of
applications. (Zave, 2017), used Alloy to provide the first specification of
correct initialization and operations of the Chord ring-maintenance protocol
(Stoica et al., 2001), using a formal model in Alloy and proving it correct.

In applying Alloy to the LGS example, we note that Alloy has no native
mechanism for expressing properties such as “handle remains in the DOWN
position” in R21. Alloy, however, can specify state transitions. Consider,
however, this rewrite of R21:

R21:

If the landing gear command handle is down, the gear is not retracting.

with “remains” changed to “is”. As an implication with a weaker antecedent,
this new R21 is stronger than the original. It can be expressed in Alloy:

⬇

R21$\colon$ check {

all lgs, lgs’$\colon$ LGS | ((lgs.handle in Down) and (lgs’.handle in Down) and Main [lgs, lgs’])

implies (lgs’.gear not in Retracting)

} for 5

where $Main$ is a predicate that yields “true” if and only if $lgs$ and
$lgs^{\prime}$ represent two consequent states of the LGS. The number 5 is the
size of the search space, serving as bound for Alloy’s use of bounded model
checking for verification.

The absence of temporal operators in Alloy similarly suggests rewriting R11bis
as:

R11bis:

If the handle remains down, three transitions of the LGS will suffice to have
the gear extended and the door closed.

This form can be expressed in Alloy:

⬇

R11bis$\colon$ check {

all lgs1, lgs2, lgs3, lgs4 $\colon$ LGS |

(((lgs1.handle in Down and lgs2.handle in Down and lgs3.handle in Down and
lgs4.handle in Down) and

(Main [lgs1, lgs2] and Main [lgs2, lgs3] and Main [lgs3, lgs4]))

implies (lgs4.gear in Extended and lgs4.door in Closed))

} for 5

Three transitions involve four different states, which is why the assertion
declares four variables of type “LGS” under the universal quantifier.

Assessing Alloy according to the criteria of section 3.3:

  * •

Audience: the Alloy notation is mathematically formal and requires the
corresponding qualification both from the specifiers and the readers.

  * •

Abstraction: the Alloy abstraction is suitable both for specifying systems’
implementations and for specifying requirements.

  * •

Method: Alloy does not assume or promote a particular requirements engineering
method.

  * •

Tool: the Alloy analyzer supports model-checking of Alloy specifications,
execution of specifications, and graphical simulation.

  * •

Traceability: Alloy focuses on model-checking specifications, so it offers no
specific support for traceability.

  * •

Coverage: Alloy supports specifying and model-checking behavioral
specifications, without consideration of non-functional properties.

  * •

Scope: Alloy can express both system and environment aspects.

  * •

Verification: Alloy models can be analyzed for consistency with
counterexample-guided model-checking, and for correctness of predicate-logic
assertions with bounded model-checking.

  * •

Semantics: the Alloy semantics is rigorously defined in (Jackson, 2006).

We have specified and verified a complete LGS example in Alloy; it can be
found in Appendix B.

Appendix B includes the complete Alloy example that we have specified and
checked.

#### 4.4.C. Tabular relations

A general approach to requirements introduced by David Parnas (Parnas, 1992)
relies on specifying relations between system variables, represented in
tabular form. The relations can be $n$-dimensional for any $n$. The underlying
mathematical theory, relations over a collection of sets, is well known, and
also serves as a basis for the relational model of databases.

Figures 4.C and 4.D illustrate an application of the tabular approach to the
LGS system. To capture requirements $R_{11}bis$ and $R_{12}bis$, since tabular
representations do not support temporal operators, we introduce variables
$gear\\_status^{\prime}$ and $door\\_status^{\prime}$, denoting the values of
$gear\\_status$ and $door\\_status$ when the program finishes its execution.

The header of the table in Fig. 4.C enumerates the possible conditions, where
$NC(handle\\_position)$ reflects the assumption that the position of the
handle does not change (Parnas, 1993): $handle\\_position=down\land
NC(handle\\_position)$, and $handle\\_position=up\land NC(handle\\_position)$.
Requirements $R\\_{21}$ and $R\\_{22}$ talk about an immediate, rather than
temporal, response of the system to the stimulus coming from the handle.

| $handle\\_position=down\land NC(handle\\_position)$ | $handle\\_position=up\land NC(handle\\_position)$
---|---|---
$gear\\_status^{\prime}$ | $extended$ | $retracted$
$door\\_status^{\prime}$ | $closed$ | $closed$
Figure 17. Fig. 4.C Expressing requirements $R_{11}bis$ and $R_{12}bis$ with a
vector function table (Parnas, 1992). The $NC(handle\\_position)$ predicate
states that the value of variable $handle\\_position$ does not change (Parnas,
1993).

The resulting vector relation table in Fig. 4.D thus does not contain any
additional variables. An important property of a table is to be $proper$ —
that is, to characterize mutually disjoint situations. The LGS knows two
situations: when the pilots’ handle in the cockpit stays (1) down and (2) up.
The LGS environment guarantees mutual disjointness of these situations.

| $handle\\_position=down$ | $handle\\_position=up$
---|---|---
$gear\\_status$ | $gear\\_status\neq retracting$ | $gear\\_status\neq extending$
Figure 18. Fig. 4.D Expressing requirements $R_{21}$ and $R_{22}$ with a
vector relation table (Parnas, 1992). The table describes the relation
connecting the handle’s position and the gear’s status.

Assessing the tabular relations approach according to the criteria of section
3.3:

  * •

Audience: the tabular notation is formal and requires mathematical
qualification.

  * •

Abstraction: the notation operates at the level of program variables. Tables
specify programs through specifying how the programs’ executions affect the
variables’ values under mutually disjoint preconditions.

  * •

Method: the approach does not assume or promote a particular requirements
engineering method.

  * •

Tool: while the approach, with its precise definition and simple tabular
representation, would naturally lend itself to tool support, we found no
record of such tools in the published literature.

  * •

Traceability: since tables directly use program variables, traceability to
implementation would fit naturally, assuming appropriate tool support.

  * •

Coverage: the tabular notation focuses on specification of functional
requirements. It defines ten classes of tables for this purpose (Parnas,
1992).

  * •

Scope: the approach can cover all aspects of requirements, including both
system and environment aspects.

  * •

Verification: verification techniques that work with tabular relations include
automated consistency checking (Heitmeyer et al., 1996) and test oracle
generation (Peters and Parnas, 1998).

  * •

Semantics: the semantics of tabular relations is formally defined (Parnas,
1992), (Parnas, 1993).

###  4.5. Seamless, programming-language-based approaches

The following discussion of programming language-based approaches covers two
recent developments: multirequirements method (Meyer, 2013) and a refinement
of it, Seamless Object-Oriented Requirements (SOOR) (Naumchev, 2019; Naumchev
and Meyer, 2017).

The underlying idea is the “Single Model Principle” described by Paige and
Ostroff (Paige and Ostroff, 2001) and going back to (Meyer, 1997). The
principle holds that there is a fundamental unity in the software process,
from requirements to design, implementation, validation and maintenance. Gaps
between these tasks (“impedance mismatches”) are a threat to quality; to avoid
them, it is desirable to use a seamless process with a consistent set of
notations and tools throughout.

####  4.5.1. Multirequirements

The multirequirements method treats requirements as compilable pieces of the
program-to-be. The pieces, being merged by special tools, form an initial
program blueprint. The method has limited consideration of environment-
controlled properties: the resulting programs cannot assume anything about
phenomena they cannot control. It does makes it possible to constrain
software-controlled environment phenomena: Design by Contract, on which the
method relies, provides the necessary specification mechanisms.

The method encourages the development of individual requirements incrementally
over several layers including formal, graphical and natural-language. The
layers complement each other and are adapted to different shareholder needs,
for example, respectively, precise descriptions advanced programmers and the
quality-assurance team, communication and decision-making, and understanding
by non-software-technical user representatives.

Design by Contract techniques capture behavioral aspects through
preconditions, postconditions and class invariants, which (as a bonus) will
remain part of the resulting program, helping a smooth interaction between
requirements, design and implementation, and supporting traceability.

The following principles of the multirequirements method reflect its
abstraction level and the central role it assigns to the traceability goal:

(3.3):

Model systems through object-oriented techniques: classes as the basic unit of
decomposition, inheritance to capture abstraction variants, contracts to
capture semantics.

(3.4):

Use an object-oriented language (in the present discussion, Eiffel) to write
the formal layer according to the principles of 3.3.

(3.5):

Use the contract sublanguage of the programming language as the notation for
the formal layer.

(3.6):

As the goal is to describe models, not implementations, ignore the imperative
parts of the programming language (such as assignment).

(3.9):

Enforce and assess traceability between the layers and all products of the
requirements process, and between requirements and other product artifacts,
both down and up.

The method further refines the notion of traceability through the following
definitions:

  * •

Up-traceability: every element of every artifact of a project follows from
some element of the requirements.

  * •

Down-traceability: for every requirement at least one artifact follows from
it.

The Eiffel Information System (EIS) tool supports these complementary notions
of traceability.

For verification, AutoProof (Tschannen et al., 2015) supports static
verification against requirements’ contracts.

Applying the multirequirements method to requirements $R_{21}$ and $R_{22}$
yields the following formal Eiffel representation:

⬇

class LGS

invariant

r21$\colon$ (handle_position $=$ down) implies (gear_status $\neq\,$
retracting)

r22$\colon$ (handle_position $=$ up) implies (gear_status $\neq\,$ extending)

end

using assertion tags r21: and r22:, which is also useful for debugging. For
$R_{11}bis$ and $R_{12}bis$:

⬇

class LGS

feature

main

do

ensure

r11_bis$\colon$ (old handle_position $=$ up and handle_position $=$ up)
implies (gear_status $=$ retracted)

r11_bis$\colon$ (old handle_position $=$ up and handle_position $=$ up)
implies (door_status $=$ closed)

r12_bis$\colon$ (old handle_position $=$ down and handle_position $=$ down)
implies (gear_status $=$ extended)

r12_bis$\colon$ (old handle_position $=$ down and handle_position $=$ down)
implies (door_status $=$ closed)

end

end

(Naumchev et al., 2015) contains a detailed application of the
multirequirements method to a well-known example of a cyber-physical system.

####  4.5.2. Seamless object-oriented requirements

The seamless object-oriented requirements (SOOR) method (Naumchev, 2019a)
extends the multirequirements approach by providing mechanisms to support
requirements reuse and the specification of environment, temporal and timing
properties. It contributes the following principles:

  * •

Use auxiliary routines with pre- and postconditions to specify and verify
software behavior under different assumptions about the environment (Naumchev
and Meyer, 2016).

  * •

Inside these auxiliary routines, use loops equipped with loop invariants and
variants to to specify and verify temporal and timing properties (Naumchev et
al., 2019).

  * •

Apply object-oriented genericity and abstraction techniques to make these
routines universally reusable and to reduce their specification complexity
(Naumchev, 2019b).

The contracted auxiliary routines at the core of the method are called
_specification drivers_ (Naumchev and Meyer, 2016). They express formal
properties of other features and classes; the technique is useful for adding
contracts externally to uncontracted texts, or, if contracts are already
present but partial, making the specification stronger. Proving through
Autoproof (Tschannen et al., 2015) enables formal verification of correctness.
In applications to testing, specification drivers can serve as parameterized
unit tests (PUT’s) (Tillmann and Schulte, 2005).

As an illustration, the formal representation of the “$R_{22}$” requirementin
SOOR will be:

⬇

class

R22

inherit

ABSENCE_BEFORE [LGS, GEAR_EXTENDING, HANDLE_DOWN]

LGS_REQUIREMENT

end

The ABSENCE_BEFORE class captures the pattern of the same name from a library
of specification patterns for finite-state verification (Dwyer et al., 1998).
This pattern takes the following form in LTL:

(1) $\Diamond R\Rightarrow(\neg P\cup R)$

The R22 class applies this pattern to the LGS implementation class by
inheriting from
ABSENCE_BEFORE with LGS for the implementation generic parameters,
GEAR_EXTENDING for $P$ from Equation 1 and HANDLE_DOWN for $R$ from the same
equation.

The ABSENCE_BEFORE [LGS, GEAR_EXTENDING, HANDLE_DOWN] fragment reads as
follows: _in LGS, the GEAR is never EXTENDING until the HANDLE is pushed
DOWN._

The ABSENCE_BEFORE generic class already contains a specification driver
capturing this property in a form suitable for either testing or program
proving. As a consequence, applying this pattern requires no manual writing of
LTL formulae. It amounts to inheriting from the ABSENCE_BEFORE class,
providing system-specific properties as the generic parameters. The
LGS_REQUIREMENT class, from which R22 inherits as well, captures LGS specific
aspects. Below is the specification driver from the R22 class that captures
the verifiable meaning of the requirement:

⬇

frozen verify (system$\colon$ LGS)

\-- (from ABSENCE_BEFORE)

do

from

timer $\colon$$=$ time_boundary

invariant

p_does_not_hold_or_else_r_holds$\colon$ not ({GEAR_EXTENDING}).default.holds
(system) or else ({HANDLE_DOWN}).default.holds (system)

variant

timer

until

({HANDLE_DOWN}).default.holds (system)

loop

iterate (system)

end

end

(Naumchev, 2019b) explains the technical details. Reuse is an important part
of the approach: template classes such as ABSENCE_BEFORE, free specifier from
having to specify verification-related technicalities that apply to many
specifications. The verify routine is submittable to AutoProof, the Hoare-
logic-based prover of Eiffel programs (Tschannen et al., 2015). AutoProof will
only accept the routine as correct if the LGS class has correct and strong
enough contracts.

The SOOR representation of the “$R_{12}bis$” requirement takes the following
form:

⬇

class

R12_BIS

inherit

RESPONSE_GLOBAL [LGS, GEAR_EXTENDED_DOOR_CLOSED_OR_ELSE_HANDLE_DOWN,
HANDLE_UP]

LGS_REQUIREMENT

end

The RESPONSE_GLOBAL class captures the following LTL pattern of the same name
(Dwyer et al., 1998):

(2) $\Box(P\Rightarrow\Diamond S)$

RESPONSE_GLOBAL [LGS, $\ldots$] expresses that _in the LGS, when the HANDLE is
pulled UP, the GEAR will eventually be seen EXTENDED and the DOOR will be seen
CLOSED; OR ELSE, we conclude that the HANDLE is pushed back DOWN._

Assessing both the multirequirements (Section 4.5.1) and the SOOR (Section
4.5.2) approaches according to the criteria of section 3.3:

  * •

Audience: the three-layer representation yields complementary specifications,
readable by different classes of stakeholders.

  * •

Abstraction: the use of programming-language notation makes it possible to
cover the full spectrum from the most abstract requirements to the most
concrete aspects of implementation.

  * •

Method: the approaches rest on a strong methodological basis, integrating the
principles object-oriented analysisthe followingLTL pattern of the same name
(t)he EIS (Eiffel Information System) tool partially supports the process. It
provides a mechanism for linking development objects o:rce pairwise
traceability between requirements expressed in different notations by making
the notion of a requirement multi-notational. EIS supports traceability
between requirements and implementations.

  * •

Coverage: the approaches focus on functional requirements.

  * •

Scope: the approaches focus on system aspects. Environment properties could in
principle be modeled in a similar way, but that aspect remains to be
developed.

  * •

Verification: in the formal layer, requirements can be verified through tools
such as AutoProof.

  * •

Semantics: the semantics of multirequirements comes from the semantics of
contracts in (Meyer, 2003).

  * •

Seamlessness: along with traceability and verification, seamlessness is one of
the highlights of these approach, which support carrying out the entire
software development lifecycle using the same set of notations (the
programming language) and tools (the IDE).

##  5\. Results and discussion

To draw conclusions from the present study, we first list limitations (5.1).
Then present a summarized table of results (5.2). Finally we explore some of
the conceptual questions raised by the notion of formal methods:

  * •

Should the elicitation process start with an informal or semi-formal notation
(5.3)?

  * •

Is a seamless approach better or worse than a mix of formal and semi-formal
notations (5.4)?

  * •

What are the merits of natural language and graphical notations for
requirements (5.5)?

  * •

What is the current state of tools support for requirements engineering (5.6)?

  * •

What is the current state of education in formal approaches to
requirements(5.7)?

###  5.1. Limitations

While we have striven to make this review comprehensive, the following
decisions may affect the generality of its results:

  * •

The choice of a running example, the Landing Gear System. An alternative would
have been to include a multitude of small examples, each chosen to make the
corresponding approach shine, whereas the LGS may be more suitable to some
than to others. The case for a single example is clear: to permit a
significant comparison of the approaches.

  * •

The nature of that example, a reactive system. An alternative would have been
an enterprise-style system (accounting, Web content management, …). The case
for a reactive system is that such applications are among the hardest to
build, so they are likely to test to their limits the advantages and
deficiencies of the methods surveyed.

  * •

The LGS example, however, does not include concurrency, which prevents
approaches such as Petri Nets or FSP/LTSA from showcasing some of their key
properties.

###  5.2. A summary of the results

Table 2 presents the key conclusions in tabular form, ordered by category
(from section 4), then alphabetically within each category. For non-binary
criteria, the table uses these notations:

  * •

System vs Environment: either S (the approach can be only used to model the
system) of B (the approach can by used to model both system and environment).

  * •

Prerequisites: one of F (formal methods background, M (general mathematical
knowledge), S (specific training required other than F and M), N (no
particular background expected)

  * •

Level of abstraction: one of L (low), H (high), B (both).

System vs Environment Prerequisites Level of abstraction Associated method
Traceability support Non-functional req. support Semantic definition Tool
support Verifiability NL to OCL S S H ✘ ✘ ✘ ✓ ✓ ✓ NL to OWL B S H ✓ ✓ ✓ ✓ ✘ ✘
NL to STD B S H ✓ ✓ ✓ ✘ ✘ ✓ Relax B N H ✘ ✓ ✓ ✓ ✓ ✓ Stimulus B N H ✘ ✘ ✘ ✓ ✓ ✓
Requirements Grammar B N H ✘ ✘ ✓ ✘ ✓ ✘ Doors B N L ✘ ✓ ✓ ✘ ✓ ✘ Reqtify B N L ✘
✓ ✓ ✘ ✓ ✘ KAOS B S B ✓ ✓ ✓ ✓ ✓ ✘ URN S S H ✓ ✓ ✓ ✘ ✓ ✘ SysML S S H ✘ ✓ ✓ ✘ ✓ ✘
URML B S H ✘ ✓ ✓ ✓ ✓ ✘ FORM-L B S H ✘ ✘ ✘ ✓ ✓ ✓ FSP/LTSA S S H ✓ ✘ ✘ ✓ ✓ ✓
Petri Nets S S H ✘ ✘ ✘ ✓ ✓ ✓ Problem Frames B S H ✓ ✘ ✘ ✓ ✓ ✓ Statecharts S S
H ✓ ✘ ✘ ✓ ✓ ✓ Alloy S F H ✘ ✘ ✘ ✓ ✓ ✓ Event-B B F B ✓ ✘ ✘ ✓ ✓ ✓ Tabular
Relations B M H ✓ ✘ ✘ ✓ ✘ ✘ VDM B F H ✓ ✘ ✘ ✓ ✓ ✓ Multirequirements B S B ✓ ✓
✘ ✓ ✓ ✘ SOOR B N B ✓ ✓ ✘ ✓ ✓ ✓

Table 2. Evaluation summary

###  5.3. Informal versus semi-formal versus formal

A requirements document should be both precise and understandable. These
objectives can conflict with each other. Among the approaches surveyed, formal
methods favor precision at the possible risk of obscurity for non-experts;
others, particularly natural-language-based and graphical, favor
understandability, at the possible risk of renouncing precise semantics.

The issue of informality versus formality in the process of requirements
engineering is not new. (In and LinLee, 1994) concludes that techniques
providing a high degree of guidance and process description are critical to
achieve successful results. (van Lamsweerde, 2000) concludes that higher-level
abstractions for requirements specification and analysis are critical success
factors.

Formal methods have produced a number of industrial success stories, but their
spread remains modest as assessed against the vast majority of projects using
classical natural-language-based techniques. This survey may provide insight
on how to extend that spread.

The usual argument against formal methods is that they are hard to understand.
It has limits, however. Stakeholder comfort is a concern, but has to be
matched against considerations of quality of the final system (“will the plane
crash?”). Only a formal version can serve as a basis for a cohesive and
unambiguous statement of client’s needs and, when necessary, for a binding
legal contract as to what the system is supposed to do.

This counter-argument (in favor of formal methods) also has its limits. The
rigor and precision of formal methods is not an excuse for ignoring the need
to understand what stakeholders want. After all, even a system that has been
formally “proved correct” has only been proved to satisfy a given
specification. However sophisticated the proof, if the specification does not
reflect the stakeholders’ desires, the system is in fact incorrect for all
practical purposes. This observation is not just theoretical: numerous
studies, most spectacularly by Lutz about NASA software (Lutz, 1993), point to
system failures resulting not from a technical error but from a bad
understanding of user needs.

Any successful requirements method, formal or not, must provide good ways to
understand and record stakeholders’ intent. Unlike what a simplistic view
might suggest, this process is not just a one-shot “requirements elicitation”
phase but often, in practice, an iterative negotiation. Informal and graphical
approaches have an advantage here since they are easy to explain to a broad
range of stakeholders. To succeed on a large scale, formal methods and tools
must provide similar mechanisms to interact with experts in the problem domain
who are not experts in requirements. The discipline of requirements
engineering traditionally recognizes (see textbooks such as (Wiegers and
Beatty, 2013) and (Laplante, 2017)) the need for “requirements engineers”,
also called “business analysts”, who help translate needs as expressed by
stakeholders, particularly “domain experts”, into bona fide requirements. To
be successful for requirements elicitation, any formal method must develop its
own cadre of such mediators, possessing both expertise in the method and an
ability to relate to ordinary project stakeholders. Proponents of formal
methods often complain about the reluctance of stakeholders to use
mathematical reasoning. Complaining does not need anywhere and deflects from
the formalists’ own responsibility: never to start a formal-method-based
requirements process without the right investment in requirements engineers
who will translate back and forth between formal and informal views.

The experience of the database community may provide guidance. In database
design, the initial phase (before the switch to an implementation that often
uses the relational model, another notation with a solid mathematical basis
(Codd, 1970)), typically relies on a graphical semi-formal notation such as
entity-relationships diagrams (Chen, 1976), possessing a precise semantics but
are intuitive enough for initial design and can be explained to non-expert
stakeholders. This experience shows that, with a proper process in place,
there is no reason to fear systematic rejection of formal or semi-formal
approaches.

###  5.4. Seamless versus conventional

The dominant view in software engineering is that requirements and code are
two fundamentally different products, to be handled through different methods,
tools and languages. The drawback is the risk of divergence: software evolves,
both on the requirements side and on the code size, and it is difficult to
maintain consistency.

An alternative approach, discussed in section 4.5, uses seamless development,
relying on a single set of concepts and notations throughout; Eiffel in
particular was designed as a language covering not only programming but also
design as well as requirements. In such an approach there is a continuum from
requirements to design to code, each step adding to the previously developed
model, making it more concrete and closer to an actual program. One of the
principal expected benefits is full traceability between requirements, design,
code and other software artifacts. The “multirequirements” approach (Meyer,
2013) extends the concept of seamlessness by using several complementary
notations such as English, a formal notation or programming language, and a
graphical notation, with the corresponding descriptions being kept in sync
(the most formal of the versions serves as the reference).

The idea of using a programming language for requirements often triggers the
reaction that programming languages are implementation-oriented and usually
imperative, jeopardizing the necessary focus of requirements on “what” rather
than “how” — the Abstraction criterion of section 3.3. This concern, however,
is not justified. Programming languages describe more than implementation.
When applying them to requirements we may ignore their imperative aspects
(although some of the authors’ work does take advantage of imperative features
(Naumchev et al., 2017; Naumchev and Meyer, 2017; Naumchev et al., 2015;
Naumchev and Meyer, 2016; Naumchev, 2019b)). Language mechanisms developed
over decades, particularly through object technology, have turned them into
modeling tools for big things. The notions of module/package, class,
inheritance, information hiding, interface, genericity are examples of these
contributions. While by definition the “things” being described are by default
programs, these scaling-up techniques introduced by programming languages are
applicable to the modularization of many other kinds of formal texts,
including requirements.

These techniques coming from programming languages are in fact the only ones
known to scale up to extremely large systems, such as a program of millions of
lines of code. Ordinary mathematical notation is not designed for that
purpose: mathematical statements typically extend over one or a few lines; to
describe the relations between them, and the overall structure of a theory in
an article or book, one has to resort to natural language. (This observation
even applies to mostly formal mathematical texts such as Whitehead and
Russell’s Principia Mathematica.) Notations for formal requirements, to be
practical, need scaling-up capabilities; they can get them, ready for use,
from programming languages with strong modular constructs. This is the vision
behind Eiffel, with its full range of object-oriented modularization
techniques, plus non-imperative specification techniques of Design by
Contract, eminently applicable, beyond programs, to requirements of large
systems.

Starting from the requirements-ready part of a programming language and
retaining the same notation through the remaining software activities of
design, implementation etc. presents the additional advantage of narrowing
gaps (“impedance mismatches”) between steps. The practical process of software
development, whether “waterfall” or “agile” in principle, is inevitably back-
and-forth in practice, with design and implementation forcing revisions of
requirements. Too often issues or new ideas arising during implementation lead
to changes that conceptually are requirements change, but do not get reflected
back into the requirements document or user stories because of the burden of
converting back and forth between completely different frameworks and
notations (typically a programming language for programs and natural language
for requirements). If everything is in a single notation it becomes more
realistic to keep everything in sync, with great advantages for traceability,
debugging and maintenance. (This is the “Single Model Principle” discussed in
4.5.)

While seamless development runs contrary to the traditional emphasis on
separation and concerns, it emphasizes the fundamental unity of software
concepts throughout the lifecycle. In that view requirements are first-class
citizens of the software world, on a par with other artifacts such as code,
designs and tests, and susceptible to the same rules and techniques.

More work, in particular empirical, remains necessary to question and validate
the seamless approach to formal and informal requirements:

  * •

Does seamlessness help make requirements useful for stakeholders with widely
different backgrounds?

  * •

What are the concrete traceability benefits?

  * •

How much does seamless development reduce documentation overhead ?

  * •

How much does it support requirements maintenance and reuse?

  * •

Tools: in a seamless approach, are program development environments enough, or
do requirements still call for specific tools?

  * •

How can the processes of requirements and implementation reinforce each other?

###  5.5. Textual versus graphical

In the discussion of how to make requirements understandable and expressible
by various kinds of stakeholders, formal-versus-informal is not the only
relevant criterion. Another opposition is textual versus graphical notations.
The two distinctions are in fact orthogonal, as all four combinations exist:

  * •

Informal specifications can be expressed in (textual) natural language, but
they can also be graphical, in part or in full.

  * •

Formal specifications, often based on a textual mathematical notation, can
also be expressed graphically. For example the presentations of Petri nets
typically use a graphical form.

While critics of formal requirements emphasize that stakeholders without a
strong software or mathematical background can react negatively to formal
texts, informal requirements are not necessarily the solution either: a long
and verbose informal text can be just as off-putting. In contrast, graphical
notations can make complex structures readily understandable. Among approaches
covered in this survey, SysML, KAOS and i* are examples of methods (of various
degrees of formality) that strongly and effectively rely on graphical
notations. Another example, from the database community, was cited above:
entity-relationship diagrams.

Graphics has clear advantages and limitations. A picture, it is said, is worth
a thousand words. But it cannot carry the details of all these words.
Graphical presentations are good at describing the overall scheme of a system
— what, with a revealing choice of words, is called “the big picture”. For
example, we can express graphically that an airplane guidance system has a
component to control the trajectory and another to monitor it and raise
alarms. Graphics is not, on the other hand, the best way to state the exact
conditions (aircraft’s altitude and angle) that will trigger an alarm.

As with formal vs informal approaches, textual and graphical notations are
best viewed as complementary techniques, outside of any dogma, each to be used
when and where it is the best way of specifying a given requirement element.

###  5.6. Tool support

Engineering the requirements of today’s complex and ambitious systems cannot
be a purely manual process. Any realistic solution requires tool support.
Modern requirements methods indeed come with tools, as cited in the previous
sections. Graphical user interfaces, for example, are available in tools
associated with methods ranging from the most informal to the fully formal,
such as Reqtify (Systems, 2016) for DOORS (4.2.1), Objectiver (Respect-it,
2011) for KAOS (4.2.2), Enterprise Architect (Systems, 2017) for SysML
(4.2.3), Overture (Project, 2017) for VDM (4.4), AutoProof (Tschannen et al.,
2015)) for multirequirements in Eiffel 4.5.1. Beyond user interfaces, however,
what matters is how these tools help the requirements process. In particular:

  * •

Which parts of requirements engineering do they facilitate?

  * •

How do they help achieve the core goal, requirements quality?

A 2011 survey of 94 requirements tools (de Gea et al., 2011) found that the
emphasis was on modeling (42% of the tools) and requirements management (39%).
This trend has continued. A commercial site listing the most widely used
requirements tools(Capterra, 2015) suggests that the principal functions of
today’s tools are requirements elicitation, change tracking and traceability.
Reqtify, for example, provides functionalities to trace requirements and link
requirements to artifacts of various kinds. The tools for KAOS (Respect-it,
2011) and i* focus on requirements elicitation. In addition to elicitation,
tools for SysML (Systems, 2017) and URML help organize requirements into
models and hierarchies, and the refinement process. All such tools, while a
great aid to the requirements process and its integration with the rest or the
development cycle, do not deal with formalization or deductive reasoning.

Approaches based on seamlessness and the Single Model Principle 4.5 make it
possible to rely on program proving tools to prove not only correctness
properties of the future program (meaning its conformance to requirements) but
also, at the requirements stage, consistency properties of the requirements
themselves, independently of any forthcoming implementation. This is the
approach taken in Eiffel with the AutoProof verification framework. Along with
proofs, such an approach may benefit from modern tools for automated testing,
such as AutoTest (Meyer et al., 2009), Pex (Tillmann and De Halleux, 2008) or
AxiomMeister (Tillmann et al., 2006). Whether proof- or test-oriented, these
tools need contracts as a basis for formal verification.

We note here a contribution of seamless development and the Single Product
Principle (even if one does not follow it to its full extent) to the general
discussion of tools for requirements: for maximum effectiveness tools
supporting requirements should support more than requirements. Consider the
example of traceability. Some requirements tools have very good support for
traceability between requirement elements. But traceability is also about
tracing relations between requirements and other artifacts, particularly
design, code and tests. (Traceability here involves detecting the consequences
of a requirements change on all such possibly affected artifacts, and the
other way around.) A tool focused just on requirements will not address this
critical need. The future, we believe, lies in integrated tools that capture,
along with requirements, all other products of software engineering.

Open questions in the area of requirements tools include:

  * •

Is there a general pattern for textual requirements, or does every domain area
requires its own?

  * •

Can tools help measure the quality of requirements?

  * •

Should tools provide (in “multirequirements” style) different viewpoints tuned
to each category of stakeholders?

  * •

Can functioning code be generated automatically from formal requirements?
Should it?

###  5.7. Education

Interest in formal approaches to express requirements and, more generally, to
design software has been progressively growing for the last few decades.
Consequently, more and more educational institutions paired their research
effort with a pedagogical effort in software engineering tracks (Liu et al.,
2009). This synergy, combined with the increasing interest of industry in
formal approaches, grew a generation of students capable of developing formal
thinking since the early stages of their professional career, and bringing
this attitude to their job environments, being it a big corporation or their
newly funded startup. The literature on pedagogical aspects of formal methods
is vast (Dean and Hinchey, 1996; Gibbons and Oliveira, 2009), in particular on
approaches to software engineering courses built on strong mathematical basis
(Gibson and Méry, 1998). Some resistance has been documented while deploying
such approaches, and the issue of motivation has also been investigated (Reed
and Sinclair, 2004; Ouhbi et al., 2015).

The general purpose requirements formalisms are not often used to teach
requirements engineering. If SysML is used, it is mainly in a larger scope of
MBSE (Model-Based System Engineering) education ( (OMG et al., 2008)). Some
other approaches like Kaos or i* are essentially used at requirements
elicitation step ((Nakatani, 2008)), notably to students having no knowledge
in formal methods ((Dalpiaz, 2015)) or to complete formal method by domain
specific ones ((Ishikawa et al., 2009)). For example, there is a workshop
series dedicated to i* teaching since 2015 (iStar@CAISE2015, iSTar@ER2017).

The idea of natural-language-based approaches is, inter alia, to avoid the
difficulty of teaching a new approach. Indeed, by providing an interface
between natural language and the formal representation of requirements, these
approaches are based on the presupposed knowledge of natural-language
requirements. The teaching of expressing requirements with natural language is
probably the first step of any requirements engineering course. In some works
(Hainey et al., 2011; Zowghi and Paryani, 2003), difficulties in teaching
requirements elicitation are highligthed, and solutions are proposed to
overcome them. However, these difficulties are not linked to the use of
natural language for requirements, but are about requirements qualities (such
as completness, consistency, etc) and the emphasis is put on how to provide
good requirements – e.g., in (Wiegers and Beatty, 2013), the authors propose
“good pratices” for requirements.

Graph and automata have always been a popular representation for students
(Grinder, 2002; Arnoux and Finkel, 2010). Despite their mathematical
foundations, they are graphical, easy to understand, and not difficult to
produce. This apparent user-friendliness often leads to misunderstanding and
errors because of the lacks of clear execution semantics, as reported by
famous articles (von der Beeck, 1994; Cuccuru et al., 2007; Dinh-Trong et al.,
2006). In that matters, the recent progress in executable semantics and in
tools animation (see previous section 5.6) is a very important progress with
regards to education.

In (Cataño and Rueda, 2009) experiences are reported in teaching formal
methods, in particular JML (Gary T. Leavens, 1998) and B (Abrial, 1996).
Design and delivery of courses aiming at developing skills of model
construction and analysis by use of notations such as VDM-SL and VDM++ are
presented in (Larsen et al., 2009). The motivation problem has been here
improved by using examples from industrial projects, and by using an
industrial-strength tool set. Concurrency theory and FSP/LTSA have also been
used in teaching and documented (Aceto et al., 2009). Among all formalisms for
concurrency, CSP has been the one with more widespread applications, both
industrial and educational (Roscoe, 1997). More interactive ways of
introducing formal specifications have been experimented, for example in
(Tarkan and Sazawal, 2009), where an on-line tutorial has been designed to
help students in the transition from Z to Alloy, considered the latter more
practical to use due to the existence of the Alloy Analyzer.

Seamless, programming-language-based approaches to requirements are not yet
widespread, so there is little empirical data available on their suitability
for teaching. But a few observations are possible. Since Design by Contract
(DbC) is the basis, the transition to a similar approach for requirements will
be easy to explain to an audience which has been introduced to programming
using DbC; this is the case with both approaches mentioned in Section 4.5:
with the multirequirements method, requirements take the form of contracted
excerpts from the final program; with seamless requirements, they take the
form of contracted routines expressed in terms of the final program.

On education, a number of questions remain open:

  * •

Are extensions to existing courses relying on DbC (Design by Contract) a
suitable approach to teach both programming and formal methods with an
emphasis on quality?

  * •

Should software engineering courses emphasize seamlessness?

  * •

Why is there so little emphasis on requirements in regular Software
Engineering curricula?

  * •

How much should formal notations appear in introductory courses?

###  5.8. Conclusion: what role for formal approaches to requirements?

What degree of formality is appropriate in stating requirements for software
systems? To shed light on that question, this survey has analyzed a wide range
of techniques for expressing software requirements, with a degree of formalism
ranging over a broad scale: from completely informal (natural language),
through partially formal (semi-formal, programming-language-based), to
completely mathematical (automata theory, other mathematical bases).

The question of formality has caused and continue to cause heated debates,
almost as old as the very recognition of requirements engineering as a
significant component of software engineering. In those discussions, the basic
arguments for and against have not changed much over decades: inevitably,
proponents of formal methods will point to the imprecision of natural
language; just as inevitably, opponents will argue that formal texts are
incomprehensible to many stakeholders. There is truth is such statements on
both sides, but they cannot end the discussion. The detailed analysis and
examples of this article should help reach better informed decisions.

As an example of the limits of classic but simplistic views, consider the
“many stakeholders do not understand formal notations” argument. In reality,
no one can require that all stakeholders understand all details of
requirements. There is no such rule in other engineering endeavors; the
marketing manager for a car company, perhaps the primary stakeholder since
what counts is how cars will sell, cannot understand all the engineering
diagrams and technical decisions. Even if we limit our focus to software, many
aspects of any sophisticated software system will remain impenetrable to some
stakeholders: if the system’s scope extends across many technical areas, as in
the case of a banking system that touches on accounting, investment
management, currency handling, international transfers etc., no single
stakeholder is an expert in all these disciplines.

One suspects that often that the formal-is-hard argument is really formal-is-
hard-for-my-developers. People who, for example, promote semi-formal Design by
Contract techniques regularly hear such comments: this is too hard for our
people, they would need retraining, or maybe they just do not have the right
mathematical education. Such objections are worth considering, but raise
questions: why do these concerns matter more than others such as verifiability
of the requirements? Comparing again with other areas of engineering, a
building contractor is unlikely to use as an excuse, if the circuits short,
that he could not require his electricians to learn Ohm’s law.

Beyond simplistic arguments, we need a balanced view assessing formality
against relevant criteria of quality. This is the focus of the present
article: each of the reviewed approaches has been evaluated according to a set
of criteria introduced in 3.3. These criteria, while not the only possible
ones, are intended to cover what is most important to the stakeholders of a
system.

In light of that review, several observations serve as a counterweight to
“formalism-is-hard”:

  * •

Stakeholders who do not understand a formal description of a system still need
to understand many of its aspects (as the car marketer must understand what is
new in the latest model). The notion of view is useful here. Requirements for
a system may have to rely on several views adapted to the needs of different
stakeholders; examples include natural language, graphical, tabular views and
of course a formal view, the appropriate one for stakeholders who need
precision and must consequently be ready to deal with mathematical concepts.
(Mathematics is not a torture imposed on innocent stakeholders; it is the only
language with full precision and, as a consequence, the language of science.)
From this perspective, a formal expression of the requirements does not
compete with other variants, but complements and supports them.

  * •

If requirements use multiple views, the question arises of how to guarantee
that they are consistent; only a formally defined view has the rigor and
precision needed to be usable as the basis to derive others. The
multirequirements method (Meyer, 2013) develops this idea further, proposing
to write requirements in a combination of natural-language, graphical and
formal notations, the formal one expressed in Eiffel and serving as the
reference in case of ambiguity.

  * •

For most practical uses, the level of mathematics actually required to
understand formal descriptions, and even in many cases to write them is not
particularly high. Many software engineers and other professionals have gone
through science curricula in which they had to master challenging mathematical
techniques, such as control theory and statistics. For most formal methods the
underlying mathematics consists of basic set theory and basic logic in the
form of propositional and predicate calculus. (Specifications of real-time
systems may also use temporal logic, but it is a simple extension to logic and
not hard to learn.) The difficulty is often apparent rather than real; a
matter of attitude.

  * •

Anyone working in software is used to highly formalized (although usually not
mathematical) notations: programming languages, which leave no room for
imprecision.

  * •

Executable semantics for general techniques such as UML or SysML have enjoyed
widespread use, showing that when benefits are clear users willlearn highly
technical approaches.

The last comment suggests a way to progress in the formal-versus-informal
debate. Ideological discussions should yield to pragmatic considerations.
Techniques will gain acceptance if they produce tangible benefits commensurate
with the effort they require. Two crucial conditions are:

  * •

Tools: even the most impressive method and elegant notation will not catch on
without automated support. Good tools free programmers from mundane tasks,
flag errors and inconsistencies, and scale up to large systems.

  * •

Education: software engineering education often causes disconnects where it
should emphasize synergy. Disconnect between requirements and subsequent
tasks, particularly implementation. Disconnect between formal methods, often
taught as a special advanced topic for theory-inclined students, and the
practice of software engineering (section 5.4 discussed the arguments for a
more seamless approach, which threads these tasks together).

Even these regrets about disconnects between courses rely on an optimistic
assumption: that students take courses on requirements and courses in formal
methods. It is in fact possible today to complete a computer
science/informatics/software engineering curriculum without having had courses
on both of these topics — or, in some cases, on either of them. Such curricula
should be corrected: every software engineer needs to know about requirements
engineering, the discipline of making sure that the implementation of systems
meets the needs of their stakeholders and the constraints of the environment;
every software engineer should know how to apply formal techniques when
precision and guaranteed correctness are required; and every software engineer
should know when and how requirements can benefit from formal methods.

Beyond their application to education, these observations describe the
relationship between formal methods and requirements in software engineering.
Formal methods are sometimes considered theoretical while requirements
engineering is essential to the practice of software construction. For that
practice, formal methods complement other requirements techniques rather than
attempting to replace them. They can and should be a powerful help available
to every requirements engineer or business analyst.

We hope that the present survey has demonstrated this potential contribution
of formal methods to requirements. We also hope that it will contribute to
expanding their role for the greater benefit of future software systems and
the people who depend on them.

### Acknowledgments

We are grateful to the authors of the surveyed approaches who took time to
check our rendering of their approaches and the treatment of the LGS examples.
(All responsibility for these descriptions remains ours.) They include in
particular Jeff Kramer, who went so far as to develop his own LTS
specification of the LGS example from which our specification benefited
considerably, and for his insightful comments, and Thuy Nguyen for his
formalization of the LGS in Form-L.

## References

  * (1)
  * Abrial (1996) Jean-Raymond Abrial. 1996\.  The B-book: Assigning Programs to Meanings.  Cambridge University Press.
  * Abrial (2010) Jean-Raymond Abrial. 2010\.  Modeling in Event-B: System and Software Engineering (1st ed.).  Cambridge Univ. Press.
  * Abrial et al. (1980) Jean-Raymond Abrial, Stephen Schuman, and Bertrand Meyer. 1980\.  A Specification Language.  In On the Construction of Programs. Cambridge University Press, 343–410.
  * Aceituna et al. (2011) D. Aceituna, H. Do, G.S. Walia, and S.-W. Lee. 2011\.  Evaluating the use of model-based requirements verification method: A feasibility study. In Workshop on Empirical Requirements Engineering (EmpiRE 2011). IEEE, 13–20.
  * Aceto et al. (2009) Luca Aceto, Anna Ingolfsdottir, Kim G. Larsen, and Jiří Srba. 2009.  Teaching Concurrency: Theory in Practice. In Teaching Formal Methods. TFM 2009. LNCS 5846, J. Gibbons and J.N. Oliveira (Eds.). Springer, 158–175.
  * Ahrendt et al. (2005) W. Ahrendt, T. Baar, B. Beckert, M. Giese, E. Habermalz, R. Hähnle, W. Menzel, and P. H. Schmitt. 2005.  The Key Tool.  Software & Systems Modeling 4, 1 (2005), 32–54.
  * Amyot (2003) D. Amyot. 2003.  Introduction to the User Requirements Notation: learning by example.  Comp. Networks 42, 3 (June 2003), 285–301.
  * Amyot and Mussbacher (2011) Daniel Amyot and Gunter Mussbacher. 2011.  User Requirements Notation: The First Ten Years, The Next Ten Years (Invited Paper).  J. of Software 6, 5 (2011), 747–768.
  * ArchSync (2006) ArchSync. 2006.  (2006).  https://sourceforge.net/projects/archsync/
  * Arnoux and Finkel (2010) Pierre Arnoux and Alain Finkel. 2010.  Using mental imagery processes for teaching and research in mathematics and computer science.  Int. J. of Mathematical Education in Science and Technology 41, 2 (2010), 229–242.
  * Bechhofer (2009) Sean Bechhofer. 2009\.  OWL: Web Ontology Language.  In Encyclopedia of Database Systems, Ling Liu and M. Tamer Özsu (Eds.). Springer, 2008–2009.  http://link.springer.com/referenceworkentry/10.1007/978-0-387-39940-9_1073
  * Berenbach et al. (2012) Brian Berenbach, Florian Schneider, and Helmut Naughton. 2012\.  The use of a requirements modeling language for industrial applications. In 2012 20th IEEE Springer Requirements Engineering Conf. (RE). IEEE, 285–290.
  * Bjørner and Jones (1978) D. Bjørner and C. B. Jones (Eds.). 1978.  Vienna Development Method: The Meta-Language. LNCS, Vol. 61.  Springer.