曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
forward. In addition, each analyst or designer will have their own abstraction, or view of the system
which must be resolved. OO does provide a structured approach to software system design and can be
very useful in helping to bring about a safer, more reliable system.
D.3 Formal Methods - Specification Development
“Formal Methods (FM) consists of a set of techniques and tools based on mathematical modeling and
formal logic that are used to specify and verify requirements and designs for computer systems and
software.”
While Formal Methods (FM) are not widely used in US industry, FM has gained some acceptance in
Europe. A considerable learning curve must be surmounted for newcomers, which can be expensive.
Once this hurdle is surmounted successfully, some users find that it can reduce overall development lifecycle
cost by eliminating many costly defects prior to coding.
WHY ARE FORMAL METHODS NECESSARY?
A digital system may fail as a result of either physical component failure, or design errors. The validation
of an ultra-reliable system must deal with both of these potential sources of error.
Well known techniques exist for handling physical component failure; these techniques use redundancy
and voting. The reliability assessment problem in the presence of physical faults is based upon Markov
modeling techniques and is well understood.
The design error problem is a much greater threat. Unfortunately, no scientifically justifiable defense
against this threat is currently used in practice. There are 3 basic strategies that are advocated for dealing
with the design error:
1. Testing (Lots of it)
2. Design Diversity (i.e. software fault-tolerance: N-version programming, recovery blocks, etc.)
3. Fault/Failure Avoidance (i.e. formal specification/verification, automatic program synthesis,
reusable modules)
The problem with life testing is that in order to measure ultrareliability one must test for exorbitant
amounts of time. For example, to measure a 10-9 probability of failure for a 1-hour mission one must test
for more than 114,000 years.
Many advocate design diversity as a means to overcome the limitations of testing. The basic idea is to use
separate design/implementation teams to produce multiple versions from the same specification. Then,
FAA System Safety Handbook, Appendix D
December 30, 2000
D - 5
non-exact threshold voters are used to mask the effect of a design error in one of the versions. The hope is
that the design flaws will manifest errors independently or nearly so.
By assuming independence one can obtain ultra-reliable-level estimates of reliability even though the
individual versions have failure rates on the order of 10-4. Unfortunately, the independence assumption
has been rejected at the 99% confidence level in several experiments for low reliability software.
Furthermore, the independence assumption cannot ever be validated for high reliability software because
of the exorbitant test times required. If one cannot assume independence then one must measure
correlations. This is infeasible as well---it requires as much testing time as life-testing the system because
the correlations must be in the ultra-reliable region in order for the system to be ultra-reliable. Therefore,
it is not possible, within feasible amounts of testing time, to establish that design diversity achieves ultrareliability.
Consequently, design diversity can create an illusion of ultra-reliability without actually providing it.
It is felt that formal methods currently offer the only intellectually defensible method for handling the
design fault problem. Because the often quoted 1 - 10-9 reliability is well beyond the range of
quantification, there is no choice but to develop life-critical systems in the most rigorous manner available
to us, which is the use of formal methods.
WHAT ARE FORMAL METHODS?
Traditional engineering disciplines rely heavily on mathematical models and calculation to make
judgments about designs. For example, aeronautical engineers make extensive use of computational fluid
dynamics (CFD) to calculate and predict how particular airframe designs will behave in flight. We use the
term formal methods to refer to the variety of mathematical modeling techniques that are applicable to
computer system (software and hardware) design. That is, formal methods is the applied mathematics
engineering and, when properly applied, can serve a role in computer system design.
Formal methods may be used to specify and model the behavior of a system and to mathematically verify
that the system design and implementation satisfy system functional and safety properties. These
specifications, models, and verifications may be done using a variety of techniques and with various
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
System Safety Handbook系统安全手册下(79)
