Formal Methods
Analysis of complex systems to ensure correctness and reduce cost
The complexity of software that will be embedded in new
aircraft and spacecraft has outpaced the capabilities of our
current verification and certification methods. Software
performs safety- and mission-critical functions on these
platforms, and correct operation is essential. Verification and
certification based on manual reviews, process constraints, and
testing are proving too expensive for even current products, let
alone advanced software-based systems. Traditional methods
cannot verify the correctness of applications such as adaptive
control for upset recovery of aircraft, intelligent control of
space craft, and control software for advanced military and
unmanned aircraft (UAVs) operating in commercial airspace.
Unless safety-critical embedded software can be developed
and verified with less cost and effort – while still satisfying the
highest reliability requirements – these new capabilities may
never reach the market.
Honeywell has recognized this challenge and has an active
research program in advanced software development and
verification tools and methodologies. Over the last 5 years,
Formal Methods has emerged as a key component in the
development and verification of the next generation of safety-
critical systems.
Formal Methods
Formal Methods is the use of ideas and techniques from
mathematics and formal logic to specify and reason about
computing systems to increase design assurance and eliminate
defects. Formal Methods tools allow comprehensive analysis
of requirements and design and complete exploration of
system behavior, including fault conditions. Formal Methods
provides a disciplined approach to analyzing complex safety-
critical systems.
The benefits of using Formal Methods include:
Product-focused measure of correctness. The use of Formal
Methods provides an objective measure of the correctness
of a system, as opposed to current process quality
measures.
Early detection of defects. Formal Methods can be applied to
the earliest design artifacts, thereby leading to earlier
detection and elimination of design defects and associated
late cycle rework.
Guarantees of correctness. Unlike testing, formal analysis
tools such as model checkers consider all possible
execution paths through the system. If there is any way to
reach a fault condition, a model checker will find it. In a
multi-threaded system where concurrency is an issue,
formal analysis can explore all possible interleavings and
event orderings.. This level of coverage is impossible to
achieve through testing.

initial configuration
error state
states reachable by test

states reachable by
formal analysis

Analytical approach to complexity. The analytical nature of
Formal Methods is better suited for verification of
complex behaviors than testing alone. Provably correct
abstractions can be used to bound the behavioral space of
systems with adaptive or non-deterministic behaviors.
Formal Methods can also be used to perform “what-if”
analyses to study the effects of proposed system changes.
Though the basic techniques have been under development
world-wide for over two decades, they have just reached the
maturity at which, in combination with increased processor
speeds and cheaper memory, they can be used to address real-
world systems.
Honeywell’s Experience
Honeywell has developed a wide array of capabilities in the
application of Formal Methods to safety-critical systems. We
can draw upon our expertise with many different Formal
Methods technologies to choose the right tools and level of
abstraction for each verification task. Honeywell’s strength
lies in our ability to apply this expertise to real systems based
on our deep understanding of the aerospace domain,
requirements for safety-critical systems, and actual
development processes. Examples of how we have applied
existing Formal Methods tools and developed new ones
include:
Source code: Source code is frequently the only complete
design artifact available for verification. Therefore, analysis of
source code is an important capability. We have found
explicit-state model checkers to be the best tools for verifying
source code. We are currently developing automated tools for
generating verification models from source code and are using
Formal Methods such as model checking
examine more system behaviors for safety
violations than testing alone