High Integrity Software: The SPARK Approach to Safety and Security [Hardcover]

John Barnes (Author)

Book Description

Publication Date: April 25, 2003

This book provides an accessible introduction to the SPARK programming language.* Updated 'classic' that covers all of the new features of SPARK, including Object Oriented Programming. * The only book on the market that covers this important and robust programming language. * CD-ROM contains the main SPARK tools and additional manuals giving all the information needed to use SPARK in practice.Technology: The SPARK language is aimed at writing reliable software that combines simplicity and rigour within a practical framework. Because of this, many safety-critical, high integrity systems are developed using SPARK. User Level: Intermediate Audience: Software engineers, programmers, technical leaders, software managers. Engineering companies in fields such as avionics, railroads, medical instrumentation and automobiles. Academics giving MSc courses in Safety Critical Systems Engineering, System Safety Engineering, Software Engineering. Author Biography: John Barnes is a veteran of the computing industry. In 1977 he designed and implemented the RTL/2 programming language and was an original member of the ADA programming language design team. He was founder and MD of Alsys Ltd from 1985 to 1991. Currently self employed, John is the author of 'Programming in ADA' which has sold 150000 copies and been translated into 6 languages.

Editorial Reviews

From the Back Cover

"This book is indispensable to the serious SPARK user, giving a complete description of the enhanced SPARK language and analysis capabilities."
--Phil Thornley, Specialist in Safety Critical Software, BAE Systems.

"The SPARK approach provides a means by which good software engineering can bepracticed and be seen to be practiced. The book provides a rich description ofand rationale for the language, and could form the foundation for guidelinesused in the programming and verification of safety critical systems."
--George Romanski, President, Verocel Inc.

"John Barnes has used his characteristic witty style to provide the reader with all they need to understand and to start using the elegant features of the SPARK high integrity language and toolset."
--S. Tucker Taft, President, SofCheck Inc., and lead designer of Ada 95.

Our lives depend -- quite literally -- on software. Banking, transport, medical and industrial control systems rely on software to function correctly. In a software-powered world it is vital for our systems to be secure, reliable and safe.

The SPARK language and tools are designed to support the construction of "high integrity" systems, where safety and security are paramount. SPARK has been applied successfully in diverse applications including railway signalling, smartcard security and avionics systems in the Lockheed C130J and EuroFighter "Typhoon" projects.

The CD-ROM accompanying the book contains

• a demonstration version of the SPARK toolset and its documentation
• code examples from the text of the book
• Aonix ObjectAda compiler Special Edition
• GNAT Compiler public edition

John Barnes, in his clear and urbane style, combines a full description of SPARK with practical advice on using the SPARK tools. Numerous examples and case studies show readers how they can create more reliable software.

0321136160B02212003

About the Author

John Barnes is a veteran of the computing industry.  In 1977 he designed and implemented the RTL/2 programming language and was an original member of the ADA programming language design team.  He was founder and MD of Alsys Ltd from 1985 to 1991.  Currently self employed, John is the author of 'Programming in ADA' which has sold 150000 copies and been translated into 6 languages.  

See all Editorial Reviews

Product Details

• Hardcover: 448 pages
• Publisher: Addison Wesley (April 25, 2003)
• Language: English
• ISBN-10: 0321136160
• ISBN-13: 978-0321136169
• Product Dimensions: 9.2 x 6.8 x 1.2 inches
• Shipping Weight: 2.1 pounds
• Average Customer Review: 5.0 out of 5 stars  See all reviews (1 customer review)
• Amazon Best Sellers Rank: #2,059,630 in Books (See Top 100 in Books)

More About the Author

Discover books, learn about writers, read author blogs, and more.

Customer Reviews

Most Helpful Customer Reviews

11 of 11 people found the following review helpful:

5.0 out of 5 stars Excellent Book for Professionals, May 24, 2003

By 

Mike - See all my reviews

This review is from: High Integrity Software: The SPARK Approach to Safety and Security (Hardcover)

If you are in the business of creating serious software that is safety critical or security related then this book is essential reading, it is also an excellent guide if you have an interest in how such software is created. Focusing on how the SPARK language assures correctness throughout the construction of the software and how the supporting tools allow analysis of the resulting program, the book forms an essential reference work for users of the SPARK approach to developing software.

This book consists of three main parts plus an appendix.
The first part consists of an overview of why SPARK was created and the background to the language and tools.
Part two looks in detail at the SPARK language.
Part three considers the tools available; various code analysis techniques and design issues that can help in the development of high integrity software. Three small case studies are included, together with some examples of real projects where SPARK has been used in large scale industrial projects.
The Appendix covers the syntax of SPARK, how to use the CD-ROM and some notes on the continuing developments of the evolution of SPARK.
The included CD-ROM allows you to try out some of what the book teaches and includes limited versions of the SPARK Examiner toolset.

In this book John Barnes writes in a style similar to his other texts; this is rather like a guiding teacher leaning over your shoulder as you work at the computer, pointing out things to observe and illustrating with snippets of code or background information. It is a style that has been criticised by some, but I find it rather reassuring as you are guided along the path to understanding. The inclusion of a CD-ROM also allows you to understand by doing, and although the tool is limited in capability, it is possible to get a good flavour of the capabilities of its parent product.

This book replaces the previous SPARK book: "High Integrity Ada : The SPARK Approach". Barnes covers the revisions and enhancements of the SPARK language described in his original book, if you are an existing user of SPARK, you need this issue to stay up-to-date with the important revisions of the language and tools. This book tries to distance itself somewhat from Ada95, possibly because of the image that language has with less well-informed programmers, but since you need an Ada compiler to produce executables from SPARK programs it would be fair to point out that SPARK is firmly rooted in Ada95.

Creating high integrity software is a disciplined process, and the book is very much based in the practical application of SPARK in building high integrity software. The SPARK language is based solid mathematical foundations, but there is no detailed descriptions at this level, the book rightly points out that they are there and then moves on towards giving you the practical information you need to write SPARK programs. Mastering SPARK gives you unprecedented skills in the highly desirable field of producing high integrity software.

Thus spake the Master programmer:
"A well written program is its own heaven; a poorly written program is its own hell."
- - from The Tao of Programming