1 files changed, 178 insertions, 0 deletions
diff --git a/eng/fv/approaches.rst b/eng/fv/approaches.rst
new file mode 100644
index 0000000..fe58a06
--- /dev/null
+++ b/eng/fv/approaches.rst
@@ -0,0 +1,178 @@
+.. SPDX-License-Identifier: CC-BY-SA-4.0
+
+.. Copyright (C) 2022 Trinity College Dublin
+
+.. _FormalVerifApproaches:
+
+Formal Verification Approaches
+==============================
+
+This is an overview of a range of formal methods and tools
+that look feasible for use with RTEMS.
+
+A key criterion for any proposed tool is the ability to deploy it in a highly
+automated manner. This amounts to the tool having a command-line interface that
+covers all the required features.
+One such feature is that the tool generates output that can be
+easily transformed into the formats useful for qualification.
+Tools with GUI interfaces can be very helpful while developing
+and deploying formal models, as long as the models/tests/proofs
+can be re-run automatically via the command-line.
+
+Other important criteria concerns the support available
+for test generation support,
+and how close the connection is between the formalism and actual C code.
+
+The final key criteria is whatever techniques are proposed should fit in
+with the RTEMS Project Mission Statement,
+in the Software Engineering manual.
+This requires, among other things,
+that any tool added to the tool-chain needs to be open-source.
+
+A more detailed report regarding this can be found in
+:cite:`Butterfield:2021:FV1-200`.
+
+
+Next is a general overview of formal methods and testing,
+and discusses a number of formalisms and tools against the criteria above.
+
+Formal Methods Overview
+-----------------------
+
+Formal specification languages can be divided into the following groups:
+
+  Model-based:  e.g., Z, VDM, B
+
+    These have a language that describes a system in terms of having an abstract
+    state and how it is modified by operations. Reasoning is typically based
+    around the notions of pre- and post-conditions and state invariants.
+    The usual method of reasoning is by using theorem-proving. The resulting
+    models often have an unbounded number of possible states, and are capable
+    of describing unbounded numbers of operation steps.
+
+  Finite State-based: e.g., finite-state machines (FSMs), SDL, Statecharts
+
+    These are a variant of model-based specification, with the added constraint
+    that the number of states are bounded. Desired model properties are often
+    expressed using some form of temporal logic. The languages used to describe
+    these are often more constrained than in more general model-based
+    approaches. The finiteness allows reasoning by searching the model,
+    including doing exhaustive searches, a.k.a. model-checking.
+
+  Process Algebras: e.g., CSP, CCS, pi-calculus, LOTOS
+
+    These model systems in terms of the sequence of externally observable
+    events that they perform. There is no explicit definition of the abstract
+    states, but their underlying semantics is given as a state machine,
+    where the states are deduced from the overall behavior of the system,
+    and events denote transitions between these states. In general both the
+    number of such states and length of observed event sequences are unbounded.
+    While temporal logics can be used to express properties, many process
+    algebras use their own notation to express desired properties by simpler
+    systems. A technique called bisimulation is used to reason about the
+    relationships between these.
+
+  Most of the methods above start with formal specifications/models. Also
+  needed is a way to bridge the gap to actual code. The relationship between
+  specification and code is often referred to as a :term:`refinement`
+  (some prefer the term :term:`reification`). Most model-based methods have refinement,
+  with the concept baked in as a key part of the methodology.
+
+  Theorem Provers: e.g., CoQ, HOL4, PVS, Isabelle/HOL
+
+    Many modern theorem provers are not only useful to help reason about the
+    formalisms mentioned above, but are often powerful enough to be used to
+    describe formal models in their own terms and then apply their proof
+    systems directly to those.
+
+  Model Checkers: e.g., SPIN, FDR
+
+    Model checkers are tools that do exhaustive searches over models with a
+    finite number of states. These are most commonly used with the finite-state
+    methods, as well as the process algebras where some bound is put on the
+    state-space. As model-checking is basically exhaustive testing, these are
+    often the easiest way to get test generation from formal techniques.
+
+  Formal Development frameworks: e.g. TLA+, Frama-C, KeY
+
+    There are also a number of frameworks that support a close connection
+    between a programming language, a formalism to specify desired behavior
+    for programs in that language, as well as tools to support the reasoning
+    (proof, simulation, test).
+
+Formal Methods actively considered
+----------------------------------
+
+Given the emphasis on verifying RTEMS C code,
+the focus is on freely available tools that could easily connect to C.
+These include: Frama-C, TLA+/PlusCal, Isabelle/HOL, and Promela/SPIN.
+Further investigation ruled out TLA+/PlusCal because it is Java-based,
+and requires installing a Java Runtime Environment.
+Frama-C, Isabelle/HOL, and Promela/SPIN are discussed below in more detail,
+
+Frama-C
+^^^^^^^
+
+Frama-C (frama-c.com) is a platform supporting a range of tools for analysing C
+code, including static analysers, support for functional specifications (ANSI-C
+Specification Language – ACSL), and links to theorem provers. Some of its
+analyses require code annotations, while others can extract useful information
+from un-annotated code. It has a plug-in architecture, which makes it easy to
+extend. It is used extensively by Airbus.
+
+Frama-C, and its plugins, are implemented in OCaml,
+and it is installed using the ``opam`` package manager.
+An issue here was that Frama-C has many quite large dependencies.
+There was support for test generation, but it was not freely available.
+Another issue was that Frama-C only supported C99, and not C11
+(the issue is how to handle C11 Atomics in terms of their semantics).
+
+Isabelle/HOL
+^^^^^^^^^^^^
+
+Isabelle/HOL is a wide-spectrum theorem-prover, implemented as an embedding of
+Higher-Order Logic (HOL) into the Isabelle generic proof assistant
+(isabelle.in.tum.de). It has a high degree of automation, including an ability
+to link to third-party verification tools, and a very large library of verified
+mathematical theorems, covering number and set theory, algebra, analysis. It is
+based on the idea of a small trusted code kernel that defines an encapsulated
+datatype representing a theorem, which can only be constructed using methods in
+the kernel for that datatype, but which also scales effectively regardless of
+how many theorems are so proven.
+It is implemented using `polyml`, with the IDE implemented using Scala,
+is open-source, and is easy to install.
+However, like Frama-C, it is also a very large software suite.
+
+Formal Method actually used
+---------------------------
+
+A good survey of formal techniques and testing
+is found in a 2009 ACM survey paper :cite:`Hierons:2009:FMT`.
+Here they clearly state:
+
+  "The most important role for formal verification in testing
+  is in the automated generation of test cases.
+  In this context,
+  model checking is the formal verification technology of choice;
+  this is due to the ability of model checkers
+  to produce counterexamples
+  in case a temporal property does not hold for a system model."
+
+Promela/SPIN
+^^^^^^^^^^^^
+
+The current use of formal methods in RTEMS is based on using the Promela
+language to model key RTEMS features,
+in such a way that tests can be generated using the SPIN model checker
+(spinroot.com).
+Promela is quite a low-level modelling language that makes it easy to get close
+to code level, and is specifically targeted to modelling software. It is one of
+the most widely used model-checkers, both in industry and education. It uses
+assertions, and :term:`Linear Temporal Logic` (:term:`LTL`) to express properties of
+interest.
+
+Given a Promela model that checks key properties successfully,
+tests can be generated for a property *P* by asking
+SPIN to check the negation of that property.
+There are ways to get SPIN to generate multiple/all possible counterexamples,
+as well as getting it to find the shortest.