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.

C. 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.

Gerald 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.

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.

Presentation

Survey Results

• plassurance.xls

• pLusage.xls

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.

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).

1. Why software is unreliable
2. Why the SDI software system will be untrustworthy
3. Why conventional software development does not produce reliable programs
4. The limits of software engineering methods
5. Artificial intelligence and the Strategic Defense Initiative
6. Can automatic programming solve the SDI software problem?
7. Can program verification make the SDI software reliable?
8. Is SDIO an efficient way to fund worthwhile research?

Summary: A Community of Verification Professionals

1. Automatic Verification of Timing Exceptions

2. AMBA Compliance Checking using Static Functional Verification

3. ARM's Paper on X Analysis - Tech Committee Award, SNUG '03

4. Solidify Verifies Design's Behavior

5. Using Static Functional Verification in the Design of a Memory Controller

6. Role of static methods in HDL verification

7. Introduction to Property Checkers for Functional Verification

8. Accelerating Functional Closure Using Solidify and Hardware Emulation

9. Static Functional Verification with Solidify: A New Low-Risk Methodology for Faster Debug of ASICs and Programmable Parts