Verified component-based software in SPARK: Experimental results for a missile guidance system

Kung Kiu Lau; Zheng Wang

doi:10.1145/1315580.1315594

Verified component-based software in SPARK: Experimental results for a missile guidance system

Research output: Chapter in Book/Conference proceeding › Conference contribution

Abstract

SPARK is useful for developing reliable software for safety-critical systems, using the 'correctness-by-construction' approach. It also has verification tools that can be used to produce verified software. To tackle larger-scale development of verified software, components are useful. In this paper we show how to define and implement software components in SPARK and use existing SPARK tools to produce verified component-based software. We demon- strate our approach on a missile guidance system. Copyright 2007 ACM.

Original language	English
Title of host publication	Proceedings of the ACM SIGAda Annual International Conference; SIGAda\|Proc. ACM SIGAda Annu. Int. Conf.
Publisher	Association for Computing Machinery
Pages	51-57
Number of pages	6
ISBN (Print)	9781595938763
DOIs	https://doi.org/10.1145/1315580.1315594
Publication status	Published - 2007
Event	2007 Annual International Conference of ACM's Special Interest Group on Ada, SIGAda 2007 - Fairfax, VA Duration: 1 Jul 2007 → …

Conference

Conference	2007 Annual International Conference of ACM's Special Interest Group on Ada, SIGAda 2007
City	Fairfax, VA
Period	1/07/07 → …

Keywords

proof reuse
software components
SPARK
verified software

Access to Document

10.1145/1315580.1315594

Cite this

@inproceedings{0b83f79ef6144c1e8486002e8dda38a1,

title = "Verified component-based software in SPARK: Experimental results for a missile guidance system",

abstract = "SPARK is useful for developing reliable software for safety-critical systems, using the 'correctness-by-construction' approach. It also has verification tools that can be used to produce verified software. To tackle larger-scale development of verified software, components are useful. In this paper we show how to define and implement software components in SPARK and use existing SPARK tools to produce verified component-based software. We demon- strate our approach on a missile guidance system. Copyright 2007 ACM.",

keywords = "proof reuse, software components, SPARK, verified software",

author = "Lau, {Kung Kiu} and Zheng Wang",

note = "SIGAda, A. C. M. Lau, Kung-Kiu Wang, Zheng 18 NEW YORK BJI01; 2007 Annual International Conference of ACM's Special Interest Group on Ada, SIGAda 2007 ; Conference date: 01-07-2007",

year = "2007",

doi = "10.1145/1315580.1315594",

language = "English",

isbn = "9781595938763",

pages = "51--57",

booktitle = "Proceedings of the ACM SIGAda Annual International Conference; SIGAda|Proc. ACM SIGAda Annu. Int. Conf.",

publisher = "Association for Computing Machinery",

address = "United States",

}

Lau, KK & Wang, Z 2007, Verified component-based software in SPARK: Experimental results for a missile guidance system. in Proceedings of the ACM SIGAda Annual International Conference; SIGAda|Proc. ACM SIGAda Annu. Int. Conf.. Association for Computing Machinery, pp. 51-57, 2007 Annual International Conference of ACM's Special Interest Group on Ada, SIGAda 2007, Fairfax, VA, 1/07/07. https://doi.org/10.1145/1315580.1315594

TY - GEN

T1 - Verified component-based software in SPARK: Experimental results for a missile guidance system

AU - Lau, Kung Kiu

AU - Wang, Zheng

N1 - SIGAda, A. C. M. Lau, Kung-Kiu Wang, Zheng 18 NEW YORK BJI01

PY - 2007

Y1 - 2007

N2 - SPARK is useful for developing reliable software for safety-critical systems, using the 'correctness-by-construction' approach. It also has verification tools that can be used to produce verified software. To tackle larger-scale development of verified software, components are useful. In this paper we show how to define and implement software components in SPARK and use existing SPARK tools to produce verified component-based software. We demon- strate our approach on a missile guidance system. Copyright 2007 ACM.

AB - SPARK is useful for developing reliable software for safety-critical systems, using the 'correctness-by-construction' approach. It also has verification tools that can be used to produce verified software. To tackle larger-scale development of verified software, components are useful. In this paper we show how to define and implement software components in SPARK and use existing SPARK tools to produce verified component-based software. We demon- strate our approach on a missile guidance system. Copyright 2007 ACM.

KW - proof reuse

KW - software components

KW - SPARK

KW - verified software

U2 - 10.1145/1315580.1315594

DO - 10.1145/1315580.1315594

M3 - Conference contribution

SN - 9781595938763

SP - 51

EP - 57

BT - Proceedings of the ACM SIGAda Annual International Conference; SIGAda|Proc. ACM SIGAda Annu. Int. Conf.

PB - Association for Computing Machinery

T2 - 2007 Annual International Conference of ACM's Special Interest Group on Ada, SIGAda 2007

Y2 - 1 July 2007

ER -

Verified component-based software in SPARK: Experimental results for a missile guidance system

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this