High Integrity Software: The SPARK Approach to Safety and Security / Edition 1

High Integrity Software: The SPARK Approach to Safety and Security / Edition 1

by John Barnes, J. G. Barnes
     
 

ISBN-10: 0321136160

ISBN-13: 9780321136169

Pub. Date: 06/20/2003

Publisher: Addison-Wesley

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

…  See more details below

Overview

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.

Read More

Product Details

ISBN-13:
9780321136169
Publisher:
Addison-Wesley
Publication date:
06/20/2003
Pages:
448
Product dimensions:
5.90(w) x 9.10(h) x 1.00(d)

Table of Contents

Foreword.
Preface.

I. AN OVERVIEW.

1. Introduction.
Software and its problems.
Correctness by construction.
Rationale for Spark.
Spark language features.
Tool support.
Examples.
Historical note.
Structure of this book.

2. Language Principles.
Decomposition and abstraction.
Language support for abstraction.
Program units.
Declarations and objects.
Subprograms.
Abstract data types.
Type extension.
Abstract state machines.
Refinement.
Program composition.

3. Spark Analysis Tools.
Program correctness.
The Examiner.
Path functions.
Verification conditions.
Iterative processes.
Nested processes.

II. THE SPARK LANGUAGE.


4. Spark Structure.
The definition of Spark.
Program units.
Lexical elements.
Pragmas.

5. The Type Model.
Objects.
Types and subtypes.
Enumeration types.
Numeric types.
Composite types.
Aggregates.
Names.
Expressions.
Constant and static expressions.

6. Control and Data Flow.
Statements.
Assignment statements.
Control statements.
Return statements.
Subprograms.
Primitive operations.
Procedure and function annotations.
Subprogram bodies and calls.

7. Packages and Visibility.
Packages.
Inherit clauses.
Own variables.
Package initialization.
Global definitions.
Private types.
Visibility.
Renaming.
Compilation units.
Subunits.
Compilation order.

8. Interfacing.
Interfacing pragmas.
Hidden text.
External variables.
The predefined library.
Spark_IO.
Implementation of Spark_IO.
Example of Spark_IO.
Interfacing to C.
Representation issues.

III. THE SPARK TOOLS.


9. The Spark Examiner.
Examination order.
Messages.
Option control.
Metafiles and index files.
Example of report file.
Proof options.
Other facilities.

10. Flow Analysis.
Production of verification conditions.
Control flow composition.
Information flow relations.
Sequences of statements.
Undefined variables.
Subprogram calls.
Conditional statements.
Loop statements and stability.

11. Verification.
Testing and verification.
Tool organization.
Run-time checks.
Functions and return annotations.
Proof contexts.
Proof functions.
Proof declarations and rules.
The FDL language.
Quantification.
Refinement and inheritance.
The Proof Checker.

12. Design Issues.
Some principles.
Architecture & Informed.
Location of state.
Package hierarchy.
Refinement and initialization of state.
Decoupling of state.
Boundary layer packages.
Summary of design guidelines.
Coding style.

13. Techniques.
Shadows.
Testing with children.
Unchecked conversion.
The Valid attribute.
Testpoints.
Memory-mapped constants.
Proof techniques.

14. Case Studies.
A lift controller.
Lift controller main program.
An autopilot.
Autopilot main program.
Altitude and heading controllers.
Run-time checks and the autopilot.
A sorting algorithm.
Proof of sorting algorithm.
Industrial applications.

APPENDICES.


A. Syntax.
Syntax of core Spark language.
Syntax of proof contexts.

B. Words, Attributes and Characters.
Spark words.
FDL words.
Attributes.
Character names.

C. Using the CD.
D. Work in Progress.
Answers to Exercises.
Bibliography.
Index.

Read More

Customer Reviews

Average Review:

Write a Review

and post it to your social network

     

Most Helpful Customer Reviews

See all customer reviews >