Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p><a href="http://en.wikipedia.org/wiki/Ada_(programming_language)" rel="noreferrer">Ada</a> and <a href="https://en.wikipedia.org/wiki/SPARK_(programming_language)" rel="noreferrer">SPARK</a> (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 <a href="http://www.google.co.uk/search?hl=en&amp;q=ada+code+verification+tools&amp;meta=" rel="noreferrer">ecosystem of code verification tooling for these languages</a>, although this technology also exists for <a href="http://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis" rel="noreferrer">more mainstream languages as well</a>.</p> <p><a href="http://www.erlang.org/" rel="noreferrer">Erlang</a> was <a href="http://www.cs.chalmers.se/Cs/Grundutb/Kurser/ppxt/HT2007/general/languages/armstrong-erlang_history.pdf" rel="noreferrer">designed from the ground up</a> for <a href="http://www.reddit.com/r/programming/comments/te5rb/whats_the_best_language_for_safety_critical/c4lxjrb" rel="noreferrer">writing high-reliability</a> telecommunications code. It is designed to facilitate separation of concerns for error recovery (i.e. 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.</p> <p><a href="http://en.wikipedia.org/wiki/Functional_programming" rel="noreferrer">Functional languages</a> such as <a href="http://www.haskell.org/haskellwiki/Haskell" rel="noreferrer">Haskell</a> can be subjected to formal proofs by automated systems due to the <a href="http://en.wikipedia.org/wiki/Declarative_programming" rel="noreferrer">declarative nature</a> 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.</p> <p>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.</p> <p><a href="http://en.wikipedia.org/wiki/Eiffel_(programming_language)" rel="noreferrer">Eiffel</a> and its descendants have built-in support for a technique called <a href="http://en.wikipedia.org/wiki/Design_by_contract" rel="noreferrer">Design By Contract</a> which provides a robust runtime mechanism for incorporating pre- and post- checks for <a href="http://en.wikipedia.org/wiki/Invariant_(computer_science)" rel="noreferrer">invariants.</a> 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.</p> <p>Although <a href="http://en.wikipedia.org/wiki/C_(programming_language)" rel="noreferrer">C</a> and <a href="http://en.wikipedia.org/wiki/C%2B%2B" rel="noreferrer">C++</a> 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.</p> <p>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 <a href="http://en.wikipedia.org/wiki/Garbage_collection_(computer_science)" rel="noreferrer">garbage collection.</a> The <a href="http://docs.hp.com/en/B2355-90694/crt0.3.html" rel="noreferrer">core run time libraries</a> 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 <a href="https://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis#C.2FC.2B.2B" rel="noreferrer">other such tools available for C</a>. There are <a href="http://www.intel.com/cd/software/products/asmo-na/eng/compilers/clin/277618.htm" rel="noreferrer">also</a> <a href="http://www.ghs.com/" rel="noreferrer">several</a> <a href="http://gcc.gnu.org/" rel="noreferrer">widely</a> <a href="http://www.lynuxworks.com/rtos/" rel="noreferrer">used</a> <a href="http://developers.sun.com/sunstudio/products/previous/9/index.html" rel="noreferrer">C/C++</a> <a href="http://www.iar.com/website1/1.0.1.0/50/1/" rel="noreferrer">based</a> <a href="http://www.arm.com/products/DevTools/index.html" rel="noreferrer">tool</a> <a href="http://www.codesourcery.com/sgpp/lite/mips" rel="noreferrer">chains</a>; most tool chains used for Ada also come in versions that support C and/or C++. </p> <p><a href="http://en.wikipedia.org/wiki/Formal_methods" rel="noreferrer">Formal Methods</a> such as <a href="http://www.cs.uiowa.edu/~slonnegr/plf/Book/Chapter11.pdf" rel="noreferrer">Axiomatic Semantics</a> (PDF), <a href="http://en.wikipedia.org/wiki/Z_notation" rel="noreferrer">Z Notation</a> or <a href="http://en.wikipedia.org/wiki/Communicating_sequential_processes" rel="noreferrer">Communicating Sequential Processes</a> 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, <a href="http://epublications.bond.edu.au/paddy_krishnan/subject_areas.html" rel="noreferrer">one of my former lecturers</a> did a formal correctness proof of a signaling system for the German railway network. </p> <p>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 <a href="http://en.wikipedia.org/wiki/Pentium_FDIV_bug" rel="noreferrer">Pentium FDIV bug</a>, formal methods have gained quite a lot of attention, and have been <a href="http://www.springerlink.com/index/GG90XJPWJDXKU5KD.pdf" rel="noreferrer">used to verify the correctness of the FPU</a> on all Intel processors since the Pentium Pro.</p> <p>Many other languages have been used to develop highly reliable software. <a href="http://www.google.co.uk/search?hl=en&amp;q=high+reliability+software+methodology&amp;meta=" rel="noreferrer">A lot of research has been done on the subject.</a> One can reasonably argue that <a href="https://stackoverflow.com/questions/176658/why-not-use-sparkada#177431">methodology is more important than the platform</a> although there are principles like simplicity and selection and control of dependencies that might <a href="http://news.bbc.co.uk/2/hi/business/7605871.stm" rel="noreferrer">preclude the use of certain platforms</a>. </p> <p>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. <a href="http://www.qnx.com/" rel="noreferrer">QNX</a> (the only such O/S that I am familiar with, having once worked with a <a href="http://www.commandalkon.com/spectrum.asp" rel="noreferrer">concrete batching system</a> based on it) is very small, and will fit on a single floppy. For similar reasons, the people who make <a href="http://www.openbsd.org/" rel="noreferrer">OpenBSD</a> - which is known for its robust security and thorough code auditing - also go out of their way keep the system simple. </p> <p><strong>EDIT:</strong> <a href="https://stackoverflow.com/questions/565965/software-safety-standards/566001#566001">This posting</a> has some links to good articles about safety critical software, in particular <a href="http://www.aonix.com/safety_critical_overview.html" rel="noreferrer">Here</a> and <a href="http://courses.cs.vt.edu/~cs3604/lib/Therac_25/Therac_1.html" rel="noreferrer">Here</a>. Props to S.Lott and Adam Davis for the source. The story of the <a href="http://en.wikipedia.org/wiki/Therac-25" rel="noreferrer">THERAC-25</a> is a bit of a classic work in this field.</p>
    singulars
    1. This table or related slice is empty.
    1. POWhich languages are used for safety-critical software?
      singulars
      1. PTQuestion
    1. PTAnswer
    1. USCommunity
    1. USConcernedOfTunbridgeWells
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. POWhich languages are used for safety-critical software?
      singulars
      1. PTQuestion
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    3. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    1. COCareful. When I worked in aerospace, Ada was used just because it was aerospace, not because of any specific Ada feature. You can write highly reliable software in any language. Aerospace software is reliable because of their rather extreme spec/coding processes, not because Ada is magic pixie dust.
      singulars
      1. PO
      1. USKen
    2. COOne of Ada's strengths actually is that it actively supports the mindset and methodologies required to develop safety-critical software, of course you could program safety-critical software in any programming language (heck, even in BASIC or assembly), but Ada was specifically designed and developed for this purpose. And the SPARK extension even more so.
      singulars
      1. PO
      1. USnone
    3. COOne erroneous thing: A functional language doesn't mean that there are no side-effects. Haskell boxes those with the Monad types so that the rest of a program can be marked as pure or safe. The idea is to denote where effects from outside might cause problems.
      singulars
      1. PO
      1. USadamaig
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload