|
"Drilling for Certainty"
David Brooks
NY Times
May 27, 2010 |
Interesting Op-Ed (Complexity and Human Understanding): Intro --
But the real issue has to do with risk assessment. It
has to do with the bloody crossroads where complex technical systems meet
human psychology.
These systems, which allow us to live as well as we do,
are too complex for any single person to understand. Yet every day,
individuals are asked to monitor the health of these networks, weigh the
risks of a system failure and take appropriate measures to reduce those
risks. |
|
"Back to the Moon: The Verification of a Small Microprocessor's Logic
Design"
Seminar:
presented by Hugh Blair-Smith
Presentation:
Back to the
Moon
Paper:
(.doc) --
(.pdf)
27th Digital Avionics Systems Conference
October 26-30, 2008
|
Abstract
The original and primary task of self-test
program Smalley3 was independent verification of the logic design of the
LOLA DU (Lunar Orbiter Laser Altimeter Digital Unit) microprocessor. Tasks
were added to verify continuing correct operation of this central processing
unit (CPU) under margin testing for supply voltage, ambient temperature, and
clock frequency. Finally, an on-orbit diagnostic task was added so that any
malfunctions of LOLA in lunar orbit can be identified as faults in, or not
in, the CPU.
The Lunar Reconnaissance Orbiter spacecraft will be
launched to the Moon in 2009 with six scientific instruments including LOLA,
each containing an embedded microprocessor to perform real-time subsystem
control calculations. LOLA's CPU is a small, custom-designed processor,
designed to meet the mission requirements while minimizing resources. This
8-bit machine is essentially code compatible with Intel's 8085 but is
implemented in modern technology, an advanced, radiation-hardened 0.15 µm
gate array, with the only logic element types being a 4:1 multiplexor and a
flip-flop.
This paper explains the fundamental structure of the
verification task, shows how particular instructions are verified, presents
a high-coverage scheme for detecting inadvertent RAM alteration, describes
subsystem testing of RAM, and reviews the results of the verification
effort. Some infamous CPU design flaws from both the commercial industry
and aerospace flight control systems are discussed. |
|
SAFETY-SPECIFIC ANALYSIS AS ADDITIONAL DESIGN ASSURANCE FOR MICROPROCESSORS
Håkan Forsberg, Saab Avitronics, Jönköping, Sweden
27th Digital Avionics Systems Conference
October 26-30, 2008 |
Abstract
In this paper we discuss the use of safety-specific
analysis (SSA) as additional design assurance of modern microprocessors. SSA
is a method to derive and validate safety-specific requirements about
internal operations of a component.
We suggest and discuss a mixed component assurance approach based
on on-chip service history, on-chip architectural mitigation techniques
(including turning off some parts) and safety-specific analysis on different
parts of the microprocessor. With this approach we believe that it might be
possible to gain certification credit for the complete microprocessor even
if some on-chip parts are partially or even completely new.
We also show why it will be very hard to perform safety-specific
analysis on a complete modern microprocessor. A modern microprocessor is
simply too complex and manipulates data in a too complex manner to be able
to analyze for safety-specific aspects. |
|
Microprocessor Evaluations for Safety-Critical, Real-Time Applications:
Authority for Expenditure No. 43 Phase 1 Report
DOT/FAA/AR-06/34
Office of Aviation Research and Development
December, 2006
|
Abstract
The intent of this report is to provide findings about safety issues in
using today’s microprocessors on aircraft. It considers the applicability of
RTCA/DO-254 to microprocessors, documents potential safety concerns when
using modern microprocessors on aircraft, and proposes potential approaches
for addressing these safety concerns.
The project is being performed in two phases with participation
from avionic system developers (BAE Systems, The Boeing Company, and Smiths
Aerospace) and Federal Aviation Administration organizations responsible for
aircraft safety research and development. Phase 1 established the project
scope and identified the research parameters as documented in this report.
This report presents an assessment of existing certification
guidelines towards certification of microprocessors. It indicates that new
validation processes are required in addition to the existing ones. The
report identifies that microprocessor obsolescence management may become a
significant problem in the future due to rapidly changing designs. This
report also addresses unpredictable issues in computational components of
the microprocessors that may lead to safety concerns in avionics
applications. The microprocessor testing and evaluation trends are
presented, and several safety concerns are identified related to the testing
and validation.
In the next phase, studies will be made to incorporate a set of
recommended guidelines towards selection and qualification of
microprocessors in the certification process. |
|
Microprocessor Evaluations for Safety-Critical, Real-Time Applications:
Authority for Expenditure No. 43 Phase 2 Report
DOT/FAA/AR-08/14
Air Traffic Organization Operations Planning
Office of Aviation Research and Development
June, 2008 |
Abstract
The intent of this report was to provide findings about
safety issues in using today’s microprocessors on aircraft. The research
effort considered the applicability of RTCA/DO-254 to microprocessors,
documented potential safety concerns when using modern microprocessors on
aircraft, and proposed potential approaches for addressing these safety
concerns.
The project was performed in multiple phases with participation
from avionic system developers (BAE Systems, The Boeing Company, Lockheed
Martin, and Smiths Aerospace) and Federal Aviation Administration
organizations responsible for aircraft safety research and development.
Phase 1 established the project scope and identified the research
parameters. Phase 1 reviewed the available literature and surveyed
microprocessor users to identify the issues and potential solutions
associated with the use of microprocessors in regulated safety-critical
applications. Phase 2, documented in this report, developed the project
objectives and found an approach to work toward the solution of these issues
and the achievement of these objectives. Phase 3 is intended to validate
this approach and continue the development of processes, services, and
prototype tool development. These results will be documented in a
Microprocessor Selection and Evaluation Handbook to facilitate application
to real-world, safety-critical applications.
Current trends toward using commercial off-the-shelf (COTS)
microprocessors present safety challenges, especially with growing design
complexity, the vast array of supported features, and limited design
documentation. A formal framework for the approval of COTS microprocessors
in aerospace systems is essential. This report proposes a Microprocessor
Approval Framework that is applicable to COTS microprocessors. |
|
Microprocessor Evaluations for Safety-Critical, Real-Time Applications:
Authority for Expenditure No. 43 Phase 3 Report
DOT/FAA/AR-08/55
Air Traffic Organization Operations Planning
Office of Aviation Research and Development
February, 2009 |
Abstract
This report discusses the findings concerning safety issues in
using today’s commercial off-the-shelf (COTS) microprocessors on aircraft.
The report addresses the applicability of RTCA/DO-254 to microprocessors,
documents potential safety concerns when using modern COTS microprocessors
on aircraft, and proposes potential approaches for addressing these safety
concerns.
The research was performed in multiple phases with participation
from avionic system developers (BAE Systems, The Boeing Company, Lockheed
Martin, and Smiths Aerospace) and Federal Aviation Administration
organizations responsible for aircraft safety research and development.
Phase 1 established the project scope and identified the research
parameters, as well as reviewed the available literature and surveyed
microprocessor users to identify the issues and potential solutions
associated with the use of COTS microprocessors in regulated,
safety-critical applications. Phase 2 developed the project objectives and
found an approach to work toward the solution of these issues and the
achievement of these objectives. Phase 3, documented in this report,
evaluated the proposed approach and continued the development of processes,
services, and prototype tool development. Phase 4, depending heavily on
industry experience, will attempt to determine if new approaches can be
developed to ensure system safety and provide more effective methods to
accumulate safety evidence for certification while reducing the time and
cost to develop and certify complex systems. These results will be
documented in a Microprocessor Selection and Evaluation Handbook to
facilitate application to real-time, safety-critical applications. |
|
Microprocessor Evaluations for Safety-Critical, Real-Time Applications:
Authority for Expenditure No. 43 Phase 4 Report
*** GET THIS REPORT WHEN IT COMES OUT *** |
|
Design Guidelines and
Criteria for Space Flight Digital Electronics |
|
Design, Analysis, and Test Guides |
|
Accelerated Verification of Digital Devices Using VHDLXL
Sandi Habinc and Peter Sinander
European Space Agency |
Abstract
This paper presents two aspects for improving the
verification of microprocessors; program-less verification,
and methods for handling large differences in abstraction
level between a reference model and the actual design.
Program-less verification is a type of pseudo random
verification where the notion of a software program
executing on the microprocessor has been abandoned. |
Why Engineers
Should Consider Formal MethodsC. Michael
Holloway
NASA LaRC
16th Digital Avionics Systems Conference, October 27-30,
1997 |
Abstract
This paper presents a logical analysis of a typical argument
favoring the use of formal methods for software development,
and suggests an alternative argument that is simpler and
stronger than the typical one. |
ICASE RQ: Formal Methods for the Quality Assurance of
Digital SystemsGerald Lüttgen
ICASE Research Quarterly |
Introduction (excerpt)
Formal Methods is an area of research in Computer Science
which aims at improving the reliability and safety of
digital systems by applying mathematical specification and
verification techniques. It complements traditional
approaches to quality assurance such as reviews and testing.
The absence of malbehavior is of particular importance
for safety-critical systems, such as used in traffic
control, medicine, aeronautics, and aerospace. Experience
shows that many fatal errors occur very rarely and under
exceptional circumstances; one major source being the
intrinsic interplay of concurrent processes as well as the
inherent complexity of fault-tolerant systems.
|
Design, Test, and
Certification Issues for Complex Integrated Circuits
Report No. DOT/FAA/AR 95/31
L. Harrison and B. Landell
August 1996 |
Abstract
This
report provides an overview of complex integrated circuit
technology, focusing particularly upon application specific
integrated circuits. This report is intended to assist FAA
certification engineers in making safety assessments of new
technologies. It examines complex integrated circuit
technology, focusing on three fields: design, test, and
certification.. It provides the reader with the background
and a basic understanding of the fundamentals of these
fields. Also included is material on the development
environment, including languages and tools.
Application
specific integrated circuits are widely used in Boeing 777
fly by wire aircraft. Safety issues abound for these
integrated circuits when they are used in safety critical
applications. Since control laws are now executed in silicon
and transmitted from one integrated circuit to another.
reliability issues for these integrated circuits take on a
new importance. This report identifies certification risks
relating to the use of complex integrated circuits in fly by
wire applications. |
Results for the Programmable Logic Usage and Assurance
Surveys
Presentation
Survey Results
|
Objective:
The objective of this research is to first determine where
and how Programmable Logic (PL) is used within NASA and
document the current methods of assurance. With that
information, to perform a gap analysis between NASA
practices and industry/military standards and practices.
Prepare training material for NASA assurance personnel and
engineers on the assurance of PL. |
|
SOFTWARE ASPECTS OF STRATEGIC DEFENSE SYSTEMS
Communications of the ACM, December 1985, Volume 28, Number 12.
Permission to copy without fee all or part of this
material is granted provided that the copies are not made or distributed for
direct commercial advantage, the ACM copyright notice and the title of the
publication and its date appear. and notice is given that copying is by
permission of the Association for Computing Machinery. To copy otherwise or
to republish. requires a fee and/or specific permission. |
Note: While some of this paper is specific to the SDI system back in
the 1980's, a good amount of the engineering analysis is applicable to those
who wish to treat the digital logic design problem as a software task and
use software methods. This analysis is applicable to our work today.
-- rk Summary:
This report comprises eight short papers that were completed while I
was a member of the Panel on Computing in Support of Battle Management,
convened by the Strategic Defense Initiative Organization (SDIO).
- Why software is unreliable
- Why the SDI software system will be untrustworthy
- Why conventional software development does not produce reliable
programs
- The limits of software engineering methods
- Artificial intelligence and the Strategic Defense Initiative
- Can automatic programming solve the SDI software problem?
- Can program verification make the SDI software reliable?
- Is SDIO an efficient way to fund worthwhile research?
|
|
Verification Guild |
Summary: A Community of Verification
Professionals |
|
Averant: White Papers |
-
Automatic
Verification of Timing Exceptions
-
AMBA Compliance
Checking using Static Functional Verification
-
ARM's Paper on X
Analysis -
Tech Committee
Award, SNUG '03
-
Solidify Verifies
Design's Behavior
-
Using Static
Functional Verification in the Design of a Memory
Controller
-
Role of static
methods in HDL verification
-
Introduction to
Property Checkers for Functional Verification
-
Accelerating
Functional Closure Using Solidify and Hardware Emulation
-
Static Functional
Verification with Solidify: A New Low-Risk Methodology
for Faster Debug of ASICs and Programmable Parts
|
Verification Methodology Manual:
Techniques for Verifying HDL Designs
David Dempster and Michael Stuart
© 2001 by Teamwork
International and TransEDA Limited |
Contents
-
Overview of Front-End Tools
-
Code and Rule Checking in the Design Flow
-
Introduction to Coverage Analysis
-
Coverage Analysis in the Design Flow
-
Practical Value of Coverage Analysis
-
Coverage Analysis Measurements
-
Coverage directed Verification Methodology
-
Verification Architecture for Pre-Silicon Validation
-
Overview of Test Bench Requirements
-
Analyzing and Optimizing the Test Suite
|