Article

OOT, DO-178C and SPARK

Authors:

Roderick Chapman,

Trevor JenningsAuthors Info & Claims

Ada-Europe'11: Proceedings of the 16th Ada-Europe international conference on Reliable software technologies

Pages 206 - 210

Published: 20 June 2011 Publication History

Publisher Site

Abstract

This position paper briefly covers the design of object-oriented programming in SPARK, and goes on to discuss the potential impact that the emerging DO-178C and Ada2012 standards might have on SPARK.

References

[1]

Amey, P.: Correctness by Construction: Better can also be Cheaper. CrossTalk Journal (March 2002), PDF on, http://www.stsc.hill.af.mil, http://www.sparkada.com

Google Scholar

[2]

Liskov, B., Wing, J.: A Behavioural Notion of Subtyping. ACM Transactions on Programming Languages and Systems 16(6) (November 1994).

Digital Library

Google Scholar

[3]

Meyer, B.: A Touch of Class: Learning to Program Well with Objects and Contracts. Springer, Heidelberg (2009) ISBN 978-3-540-92144-8

Digital Library

Google Scholar

Recommendations

Position paper: DO-178C/ED-12C and object-orientation for critical systems
Ada-Europe'11: Proceedings of the 16th Ada-Europe international conference on Reliable software technologies

DO-178C/ED-12C, six years in preparation, is expected to be published in 2011. This updated document will provide guidance for the development and verification of safety-related software for avionic systems. As this position paper will describe, DO-178C/...
Bringing safe, dynamic parallel programming to the spark verifiable subset of ada
HILT '13

SPARK is a verifiable subset of Ada which has been in use for over 20 years for developing the most critical parts of complex real-time applications [1][2]. A restricted subset of the Ada tasking model is included in the newer versions of SPARK ("...
Bringing safe, dynamic parallel programming to the spark verifiable subset of ada
HILT '13: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology

SPARK is a verifiable subset of Ada which has been in use for over 20 years for developing the most critical parts of complex real-time applications [1][2]. A restricted subset of the Ada tasking model is included in the newer versions of SPARK ("...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Ada-Europe'11: Proceedings of the 16th Ada-Europe international conference on Reliable software technologies

June 2011

226 pages

ISBN:9783642213373

Editors:
Alexander Romanovsky
Newcastle University, School of Computing Science, Newcastle upon Tyne, UK
,
Tullio Vardanega
University of Padua, Department of Pure and Applied Mathematics, Padua, Italy

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 20 June 2011

Author Tags

Qualifiers

Article

Recommendations

Position paper: DO-178C/ED-12C and object-orientation for critical systems

Bringing safe, dynamic parallel programming to the spark verifiable subset of ada

Bringing safe, dynamic parallel programming to the spark verifiable subset of ada