The first paper in the Aerospace session was a discussion of the COMPASS approach: correctness, modeling and perfomability of aerospace systems. Marco Bozzano discussed the SLIM formal modeling language that is potentially of use modeling such things as error behavior in aerospace systems. He described a model of a complete power system including devices, features, and error modes and diagnostics. The model can be used to inject error modes to determine survivability of the system. He discussed validation methodology within the COMPASS system.
Formal methodology is so far afield for me that it is fascinating, and I'm swimming very hard to keep up with some of the discussions.
Holger Blasum, of Sysgo AG, presented a "Formal Verification of a Microkernel Used in Dependable Software Systems."
Blasum talked about the formal review processes in avionics and how much time it takes. He discussed the PikeOS realtime operating microkernel. PikeOS projects include traffic control, automotive projects like brake systems, collision radar. PikeOS is used in several Airbus models.
The project (Verisoft XT) is to develop highly reliable software. A subproject for avionics is the verification of PikeOS using the VCC verification tool.
The third paper in the Aerospace session was entitled "Issues in Tool Qualification for Safety-Critical Hardware: What Formal Approaches Can and Cannot Do." It was presented by Dr.Andrew Kornecki of Embry-Riddle Aeronautical University in Florida. The conclusion of his talk reports:
Technology has improved to the point that system designers have the ability to trade-off inplementing complex functions in either hardware or software. However in the design tool world thre are clear distinctions between software and hardware tools. One of the major concerns in any hardware deisgn is assuring that the hardware correctly implements the HDL description. As the synthesis and place and route process proceeds, the architecture used to implement any given HDL description can be changed to optimize the design for area, power or timing. The symthiseis toold viedws all of the implementations as logically equivalent, but they may not be equivalent in the eyes of the designer. Formal tools and specifically equivalence checking approach seem to be an excellent method to guarantee that the designer's intent has been translated to the physical hardware. While both verification of models and hardware sythesis have been successfully applied in industrial practice, there are several caveats in practice when physical components come into play. The issues are not due to the incorrectness of either formal analyses nor errors in the syntesizers but theinadequacy of the analyzed models and the not so simple internal conditions and related sythesizers' construction.
Formal methods must never give us a false sense of confidence. Despite the best design and verification efforts, the hardware may still produce unexpecte results. These errors can be due to noise, supply bounce, timing issues, or even cosmic radiation. It should be noted that specialized design tool suites to address all of the a bove error conditions exist. The tradeoffs between the costs and benefits of using these tools must be investigated for each design. Despite all of the design tools available, the most important component of any safety critical design is an experienced designer with the experience and ability to differentiate between what issues are critical and what issues are ngegligible. It should also be noted that a rigorous process and safety culture promoted by appropriate guidance in regulated industries is an integral element to improve safety,
