曝光臺 注意防騙 網曝天貓店富美金盛家居專營店坑蒙拐騙欺詐消費者

degrees of rigor. The following is an imperfect, but useful, taxonomy of the degrees of rigor in formal
methods:
Level-1: Formal specification of all or part of the system.
Level-2: Formal specification at two or more levels of abstraction and paper and pencil proofs that
the detailed specification implies the more abstract specification.
Level-3: Formal proofs checked by a mechanical theorem prover.
Level 1 represents the use of mathematical logic or a specification language that has a formal semantics to
specify the system. This can be done at several levels of abstraction. For example, one level might
enumerate the required abstract properties of the system, while another level describes an implementation
that is algorithmic in style.
Level 2 formal methods goes beyond Level 1 by developing pencil-and-paper proofs that the more
concrete levels logically imply the more abstract-property oriented levels. This is usually done in the
manner illustrated below.
Level 3 is the most rigorous application of formal methods. Here one uses a semi-automatic theorem
prover to make sure that all of the proofs are valid. The Level 3 process of convincing a mechanical
FAA System Safety Handbook, Appendix D
December 30, 2000
D - 6
prover is really a process of developing an argument for an ultimate skeptic who must be shown every
detail.
Formal methods is not an all-or-nothing approach. The application of formal methods to only the most
critical portions of a system is a pragmatic and useful strategy. Although a complete formal verification
of a large complex system is impractical at this time, a great increase in confidence in the system can be
obtained by the use of formal methods at key locations in the system.
D.3.1 Formal Inspections of Specifications
Formal inspections and formal analysis are different. Formal Inspections should be performed within
every major step of the software development process.
Formal Inspections, while valuable within each design phase or cycle, have the most impact when applied
early in the life of a project, especially the requirements specification and definition stages of a project.
Studies have shown that the majority of all faults/failures, including those that impinge on safety, come
from missing or misunderstood requirements. Formal Inspection greatly improves the communication
within a project and enhances understanding of the system while scrubbing out many of the major
errors/defects.
For the Formal Inspections of software requirements, the inspection team should include representatives
from Systems Engineering, Operations, Software Design and Code, Software Product Assurance, Safety,
and any other system function that software will control or monitor. It is very important that software
safety be involved in the Formal Inspections.
It is also very helpful to have inspection checklists for each phase of development that reflect both generic
and project specific criteria. The requirements discussed in this section and in Robyn R. Lutz's paper
"Targeting Safety-Related Errors During Software Requirements Analysis" will greatly aid in establishing
this checklist. Also, the checklists provided in the NASA Software Formal Inspections Guidebook are
helpful.
D.3.2 Timing, Throughput And Sizing Analysis
Timing and sizing analysis for safety critical functions evaluates software requirements that relate to
execution time and memory allocation. Timing and sizing analysis focuses on program constraints.
Typical constraint requirements are maximum execution time and maximum memory usage. The safety
organization should evaluate the adequacy and feasibility of safety critical timing and sizing
requirements. These analyses also evaluate whether adequate resources have been allocated in each case,
under worst case scenarios. For example, will I/O channels be overloaded by many error messages,
preventing safety critical features from operating.
Quantifying timing/sizing resource requirements can be very difficult. Estimates can be based on the
actual parameters of similar existing systems.
Items to consider include:
· memory usage versus availability;
· I/O channel usage (load) versus capacity and availability;
· execution times versus CPU load and availability;
· sampling rates versus rates of change of physical parameters.
FAA System Safety Handbook, Appendix D
December 30, 2000
D - 7
In many cases it is difficult to predict the amount of computing resources required. Hence, making use
of past experience is important.
D.3.3 Memory usage versus availability
Assessing memory usage can be based on previous experience of software development if there is
　
中國航空網 www.k6050.com
航空翻譯 www.aviation.cn
本文鏈接地址：System Safety Handbook系統安全手冊下(80)