High integrity software

John Barnes

448 pages, parution le 26/03/2003

Ajouter à une liste

Indisponible

Résumé

"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 be practiced and be seen to be practiced. The book provides a rich description of and rationale for the language, and could form the foundation for guidelines used 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

Contents

An Overview

Introduction
Language Principles
SPARK Analysis Tools

The SPARK Language

SPARK Structure
The Type Model
Control and Data Flow
Packages and Visibility
Interfacing

The SPARK Tools

The SPARK Examiner
Flow Analysis
Verification
Design Issues
Techniques
Case Studies

Appendices

Syntax
Words, Attributes and Characters
Using the CD
Work in Progress

L'auteur - John Barnes

John Barnes a participe a toutes les étapes du développement du langage Ada. Il a fait partie de l'équipe à l'origine de la première version du langage, Ada 83, et a participé à l'élaboration de Ada 95. Il est actuellement président d'Ada-Europe. Programmer en Ada et Programmer en Ada 95 sont désormais des classiques dans le monde Ada.

Caractéristiques techniques

	PAPIER
Éditeur(s)	Addison Wesley
Auteur(s)	John Barnes
Parution	26/03/2003
Nb. de pages	448
Format	17,5 x 24
Couverture	Relié
Poids	888g
Intérieur	Noir et Blanc
EAN13	9780321136169
ISBN13	978-0-321-13616-9