diff options
Diffstat (limited to '')
-rwxr-xr-x | eng/fv/overview.rst | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/eng/fv/overview.rst b/eng/fv/overview.rst new file mode 100755 index 0000000..da981f2 --- /dev/null +++ b/eng/fv/overview.rst @@ -0,0 +1,38 @@ +.. SPDX-License-Identifier: CC-BY-SA-4.0 + +.. Copyright (C) 2022 Trinity College Dublin + +.. _FormalVerifOverview: + +Formal Verification Overview +============================ + +Formal Verification is a technique based on writing key design artifacts using +notations that have a well-defined mathematical :term:`semantics`. This means +that these descriptions can be rigorously analyzed using logic and other +mathematical tools. The term :term:`formal model` is used to refer to any such +description. + +Having a formal model of a software engineering artifact (requirements, +specification, code) allows it to be analyzed to assess the behavior it +describes. This means checks can be done that the model has desired properties, +and that it lacks undesired ones. A key feature of having a formal description +is that tools can be developed that parse the notation and perform much, +if not most, of the analysis. An industrial-strength formalism is one that has +very good tool support. + +Having two formal models of the same software object at different levels +of abstraction (specification and code, say) allows their comparison. In +particular, a formal analysis can establish if a lower level artifact like +code satisfies the properties described by a higher level, +such as a specification. This relationship is commonly referred to as a +:term:`refinement`. + +Often it is quite difficult to get a useful formal model of real code. Some +formal modelling approaches are capable of generating machine-readable +:term:`scenarios <scenario>` that describe possible correct behaviors of the +system at the relevant level of abstraction. A refinement for these can be +defined by using them to generate test code. +This is the technique that is used in :ref:`FormalVerifMethodology` to +verify parts of RTEMS. Formal models are constructed based on requirements +documentation, and are used as a basis for test generation. |