Introduction

Chapter 2: The Practical Application of Formal Methods

The practical application of formal methods is typically framed within specific project contexts, potentially influenced by institutional conventions and criteria. This chapter reviews contextual factors that shape formal methods usage and provides an overview of the formal methods process. The discussion transitions from the strict formal nature of formal methods to the subtler, implied methods utilized in practice. It also includes background information on SAFER, which highlights critical aspects of formalization and analysis that will be explored in subsequent chapters.

2.1 What Are Formal Methods?

Formal Methods refer to a suite of techniques derived from logic and discrete mathematics tailored for specifying, designing, and constructing software and computer systems. The term "formal" relates to formal logic, emphasizing the structural relationships among elements. In this area of reasoning, validity arises from form rather than content, requiring meticulous enumeration of assumptions and reasoning steps, all abiding by a limited number of inference rules. The most stringent formal methods systematically apply these techniques to verify requirements or components in complex systems, aiming to minimize reliance on human judgment and intuition, thus advocating a calculative and mechanically verifiable argument base.

Spectrum of Formal Methods

The definition of Formal Methods implies a variety of techniques and strategies. The specific roles and resources available for formal methods influence the techniques that might be selected for a project. Less rigorous methods prioritize formalization without exhaustive calculations, while more rigorous ones employ strict methodologies to achieve reliability and assurance.

2.2 Roles of Formal Methods

Formal methods can be employed analytically or descriptively:

• Analytical Role: Utilizing formal methods to ascertain internal consistency within descriptions, derive necessary properties from requirements, or compare various design implementations.

• Descriptive Role: Assisting in documenting requirements and facilitating communication among stakeholders during reviews or inspections.

The intended roles of formal methods shape the selection of appropriate techniques and strategies, guiding their practical application.

2.3 Formal Methods: Degree of Formalization and Scope of Use

Formal methods are assessed via their level of formalization and their intended scope. This classification yields diverse applications:

2.3.1 Levels of Formalization

1. Mathematical Concepts: Employing informal analysis without mechanization.

2. Formalized Specification: Utilizing specification languages with limited mechanized support.

3. Comprehensive Environment: Applying rigorous formal specification languages with automated proof-checking or theorem-proving functionalities.

The evolution and maturity of formal methods are reflected in their increasing reliance on computer support, progressively moving from informal to formal methodologies.

2.3.2 Scope of Formal Methods Use

Formal methods application can vary based on:

1. Development Life Cycle Stages: The greatest benefit is derived from early life-cycle application, where the costs of undetected errors escalate.

2. System Components: Prioritizing components for analysis based on criticality and assurance needs.

3. System Functionality: Focusing on significant properties rather than attempting to prove comprehensive correctness.

2.4 Reasonable Expectations for Formal Methods

Realistic expectations surrounding formal methods hinge on their chosen roles, extent of use, and project resources. They can unveil faults earlier in the development process compared to conventional methods, thereby reducing errors profoundly in requirements interpretation and implementation. However, even the most rigorous formal techniques come with caveats and do not guarantee flawlessness.

2.5 The Method Underlying Formal Methods

In engineering, a method outlines how processes are executed, consisting of:

1. An underlying development model.

2. Relevant languages.

3. Defined and ordered steps.

4. Guidance for coherent application.

Notably, the formal methods community has been slow to define comprehensive methodologies, often lacking structured guidance in applying various techniques.

2.6 An Introduction to SAFER

SAFER is a propulsive backpack system crafted to aid in self-rescue for NASA crew during Extra-Vehicular Activities (EVA). It is vital for situations where tethers fail during mission-critical operations. Weighing approximately 85 pounds and leveraging an operational attitude-hold capability, SAFER allows for detumbling and return of the astronaut. The system incorporates advanced avionics and control electronics to manage movements and functions through user-friendly controllers accessible even under challenging spatial orientations. This chapter embarks on illustrating SAFER's design through formal methods, addressing the multitude of components and functions integral to its operations.