Which languages are used for safety
I'm researching the development of safety-critical software, and in particular what effects the choice of programming language has on such development.
Please explain, in detail, which languages are commonly used, and why.
Ada and SPARK (which is an Ada dialect with some hooks for static verification) are used in aerospace circles for building high reliability software such as avionics systems. There is something of an ecosystem of code verification tooling for these languages, although this technology also exists for more mainstream languages as well.
Erlang was designed from the ground up for writing high-reliability telecommunications code. It is designed to facilitate separation of concerns for error recovery (ie the subsystem generating the error is different from the subsystem that handles the error). It can also be subjected to formal proofs although this capability hasn't really moved far out of research circles.
Functional languages such as Haskell can be subjected to formal proofs by automated systems due to the declarative nature of the language. This allows code with side effects to be contained in monadic functions. For a formal correctness proof the rest of the code can be assumed to do nothing but what is specified.
However, these languages are garbage collected and the garbage collection is transparent to the code, so it cannot be reasoned about in this manner. Garbage collected languages are not normally predictable enough for hard realtime applications, although there is a body of ongoing research in time bounded incremental garbage collectors.
Eiffel and its descendants have built-in support for a technique called Design By Contract which provides a robust runtime mechanism for incorporating pre- and post- checks for invariants. While Eiffel never really caught on, developing high-reliability software tends to consist of writing checks and handlers for failure modes up-front before actually writing the functionality.
Although C and C++ were not specifically designed for this type of application, they are widely used for embedded and safety-critical software for several reasons. The main properties of note are control over memory management (which allows you to avoid having to garbage collect, for example), simple, well debugged core run-time libraries and mature tool support. A lot of the embedded development tool chains in use today were first developed in the 1980s and 1990s when this was current technology and come from the Unix culture that was prevalent at that time, so these tools remain popular for this sort of work.
While manual memory management code must be carefully checked to avoid errors, it allows a degree of control over application response times that is not available with languages that depend on garbage collection. The core run time libraries of C and C++ languages are relatively simple, mature and well understood, so they are amongst the most stable platforms available. Most if not all of the static analysis tools used for Ada also support C and C++, and there are many other such tools available for C. There are also several widely used C/C++ based tool chains; most tool chains used for Ada also come in versions that support C and/or C++.
Formal Methods such as Axiomatic Semantics (PDF), Z Notation or Communicating Sequential Processes allow program logic to be mathematically verified, and are often used in the design of safety critical software where the application is simple enough to apply them (typically embedded control systems). For example, one of my former lecturers did a formal correctness proof of a signaling system for the German railway network.
The main shortcoming of formal methods is their tendency to grow exponentially in complexity with respect to the underlying system being proved. This means that there is significant risk of errors in the proof, so they are practically limited to fairly simple applications. Formal methods are quite widely used for verifying hardware correctness as hardware bugs are very expensive to fix, particularly on mass-market products. Since the Pentium FDIV bug, formal methods have gained quite a lot of attention, and have been used to verify the correctness of the FPU on all Intel processors since the Pentium Pro.
Many other languages have been used to develop highly reliable software. A lot of research has been done on the subject. One can reasonably argue that methodology is more important than the platform although there are principles like simplicity and selection and control of dependencies that might preclude the use of certain platforms.
As various of the others have noted, certain O/S platforms have features to promote reliability and predictable behaviour, such as watchdog timers and guaranteed interrupt response times. Simplicity is also a strong driver of reliability, and many RT systems are deliberately kept very simple and compact. QNX (the only such O/S that I am familiar with, having once worked with a concrete batching system based on it) is very small, and will fit on a single floppy. For similar reasons, the people who make OpenBSD - which is known for its robust security and thorough code auditing - also go out of their way keep the system simple.
EDIT: This posting has some links to good articles about safety critical software, in particular Here and Here. Props to S.Lott and Adam Davis for the source. The story of the THERAC-25 is a bit of a classic work in this field.
For C++, the Joint Strike Fighter (F-35) C++ Coding Standard is a good read:
http://www.stroustrup.com/JSF-AV-rules.pdf
I believe Ada is still in use in some government projects that are safety and/or mission critical. I've never used the language, but it's on my list of "to learn", along with Eiffel. Eiffel offers Design By Contract, which is supposed to improve reliability and safety.
链接地址: http://www.djcxy.com/p/79150.html上一篇: 在C方向
下一篇: 哪些语言用于安全