Industrial Use of Formal Methods E-Book

• Herausgeber: John Wiley & Sons
• Kategorie: Fachliteratur
• Sprache: Englisch

Seitenzahl: 416

Veröffentlichungsjahr: 2013

Beschreibung

At present the literature gives students and researchers of the very general books on the formal technics. The purpose of this book is to present in a single book, a return of experience on the used of the “formal technics” (such proof and model-checking) on industrial examples for the transportation domain.

This book is based on the experience of people which are completely involved in the realization and the evaluation of safety critical system software based. 

The implication of the industrialists allows to raise the problems of confidentiality which could appear and so allow to supply new useful information (photos, plan of architecture, real example).

Leseprobe

Table of Contents

Introduction

Jean-Louis BOULANGER

Chapter 1. SPARK — A Language and Tool-Set for High-Integrity Software Development

Ian O’NEILL

1.1. Introduction

1.2. An overview of SPARK

1.3. The rationale behind SPARK

1.4. Industrial applications of SPARK

1.5. Conclusion

1.6. Bibliography

Chapter 2. Model-Based Testing Automatic Generation of Test Cases Using the Markov Chain Model

Héléne LE GUEN, Frederique VALLÉE and Anthony FAUCOGNEY

2.1. Preliminaries on the test process

2.2. Modeling using Markov chains

2.3. The MaTeLo tool

2.4. Examples of industrial applications

2.5. Conclusion

2.6. Bibliography

Chapter 3. Safety Analysis of the Embedded Systems with the AltaRica Approach

Pierre BIEBER and Christel SEGUIN

3.1. Introduction

3.2. Safety analysis of embedded systems

3.3. AltaRica language and tools

3.4. Examples of modeling and safety analysis

3.5. Comparison with other approaches

3.6. Conclusion

3.7. Special thanks

3.8. Bibliography

Chapter 4. Polyspace®

Patrick MUNIER

4.1. Overview

4.2. Introduction to software quality and verification procedures

4.3. Static analysis

4.4. Dynamic tests

4.5. Abstract interpretation

4.6. Code verification

4.7. Robustness verification or contextual verification

4.8. Examples of Polyspace® results

4.9. Carrying out a code verification with Polyspace®

4.10. Use of Polyspace® can improve the quality of embedded software

4.11. Carrying out certification with Polyspace®

4.12. The creation of critical onboard software

4.13. Concrete uses of Polyspace®

4.14. Conclusion

4.15. Bibliography

Chapter 5. Escher Verification Studio Perfect Developer and Escher C Verifier

Judith CARLTON and David CROCKER

5.1. Introduction

5.2. Perfect Developer — its inspiration and foundations

5.3. Theoretical foundations

5.4. The Perfect language

5.5. A Perfect Developer example

5.6. Escher C verifier

5.7. The C subset supported by eCv

5.8. The annotation language of eCv

5.9. Escher C verifier examples

5.10. The theorem prover used by Perfect Developer and Escher C verifier

5.11. Real-world applications of Perfect Developer and Escher C verifier

5.12. Future work

5.13. Glossary

5.14. Bibliography

Chapter 6. Partial Applications of Formal Methods

Aryldo G. RUSSO Jr.

6.1. History

6.2. Case studies

6.3. Conclusion

6.4. Bibliography

Chapter 7. Event-B and Rodin

Michael BUTLER, Asieh SALEHI FATHABADI and Renato SILVA

7.1. Event-B

7.2. Rodin as an Event-B tool

7.3. Event-B model decomposition

7.4. Case study: metro system

7.5. Acknowledgments

7.6. Bibliography

Chapter 8. Conclusion

Jean-Louis BOULANGER

8.1. Introduction

8.2. Structured, semi-formal and/or formal methods

8.3. Conclusion

8.4. Bibliography

Glossary

List of Authors

Index

Industrial Use of Formal Methods

Formal Verification

Edited byJean-Louis Boulanger

First published 2012 in Great Britain and the United States by ISTE Ltd and John Wiley & Sons, Inc.

Apart from any fair dealing for the purposes of research or private study, or criticism or review, as permitted under the Copyright, Designs and Patents Act 1988, this publication may only be reproduced, stored or transmitted, in any form or by any means, with the prior permission in writing of the publishers, or in the case of reprographic reproduction in accordance with the terms and licenses issued by the CLA. Enquiries concerning reproduction outside these terms should be sent to the publishers at the undermentioned address:

ISTE Ltd

John Wiley & Sons, Inc.

27–37 St George’s Road

111 River Street

London SW19 4EU

Hoboken, NJ 07030

UK

USA

www.iste.co.uk

www.wiley.com

© ISTE Ltd 2012

The rights of Jean-Louis Boulanger to be identified as the author of this work have been asserted by him in accordance with the Copyright, Designs and Patents Act 1988.

Library of Congress Cataloging-in-Publication Data

Industrial used of formal methods: formal verification / edited by Jean-Louis Boulanger.

p. cm.

Includes bibliographical references and index.

ISBN 978-1-84821-363-0 (hardback)

1. Systems engineering—Data processing. 2. Computer simulation. 3. Formal methods (Computer science) 4. Computer software—Verification. 5. Nondestructive testing. I. Boulanger, Jean-Louis.

TA168.I45 2012

005.101—dc23

2012011854

British Library Cataloguing-in-Publication Data

A CIP record for this book is available from the British Library

ISBN: 978-1-84821-363-0

Introductiona

Context

Although formal analysis programming techniques (see works by Hoare [HOA 69] and Dijkstra [DIJ 75]) may be quite old, the introduction of formal methods dates from the 1980s. These techniques enable us to analyze behavior of a software application, described in a programming language. Program correction (good behavior, program stop, etc.) is thus demonstrated through a program proof based on the weakest precondition calculation [DIJ 76].

It took until the end of the 1990s before formal methods (Z [SPI 89], VDM [JON 90]), or the B method [ABR 96, ARA 97] could be implemented in industrial applications, or were usable in an industrial setting.

One of the stumbling blocks was implementing them in the framework of an industrial application (size of application, cost constraints, or delays, etc.). This implementation is only possible using “sufficiently” mature and high-performance tools.

It should be noted that in the context of safety-critical applications, at least two formal methods have a currently-used and recognized environmental design, which covers one part of the specification production process according to the code, all the while integrating one or more verification processes; namely the B method [ABR 96] and the LUSTRE language [HAL 91, ARA 97] and its graphic version, named SCADE1 [DOR 08].

The B method and the SCADE environment are associated with industrial tools.

For example, Atelier B and the B-Toolkit, marketed by CLEARSY2 and B-Core3 respectively, are tools, which completely cover the development cycle proposed by the B method (specification, refinement, code, and proof generation). Atelier B4 can be accessed for free from version 4.0 onward.

Formal methods rely on different formal verification techniques such as proofs, model checking [BAI 08], and/or simulation.

The use of formal methods while in full development remains marginal, given the number of lines of code. In effect, there are currently many more Ada [ANS 83], C [ISO 99] or C++ lines of code, which have been produced manually rather than through a formal process.

That is why other formal techniques have been implemented to verify the behavior of a software application written in a programming language such as C or Ada. The technical principle known as abstract interpretation [COU 00] of programs makes it possible to evaluate all the behaviors of a software application through a static analysis. This type of technique has, in the last few years, given rise to several tools such as Polyspace®5, Caveat6, Absint7, Frama-C8, and/or ASTREE9.

The efficacy of these static program analysis techniques has progressed greatly with the increase in power of business machines. It should be noted that these techniques generally necessitate the integration of complementary information such as pre-conditions, invariants and/or post-conditions in the manual code.

SPARK Ada10 [BAR 03] is one approach where the Ada language [ANS 83] has been expanded to introduce these complementary elements (pre-, post-, invariant), and an adapted suite of tools has been defined.

Objective of this book

In [BOW 95, ARA 97], industrial feedback involving formal techniques can be found, and notably, a report on the B method [ABR 96], the LUSTRE language [HAL 91, ARA 97], and SAO+, the predecessor to SCADE11 [DOR 08]. Other work such as [MON 00, MON 02, HAD 06] provide a panorama of formal methods with a more scientific point of view.

Given the presentation of the context and of the state of the literature, our objective is to present concrete examples of industrial use of formal techniques.

By formal techniques, we mean the different approaches based on mathematics making it possible to demonstrate that a software application abides by some properties.

Note that the standard use of formal techniques consists of making specification and/or design models, but formal techniques are seen more and more as a possibility of making a verification (static analysis of code, demonstration of abiding by properties, good management of floating-point calculations, etc.).

This work is related to two other books by the same authors published by ISTE and John Wiley & Sons in 2012 [BOU 12c, BOU 12d].

The current book is dedicated to the presentation of different formal techniques, such as the SPARK Ada (Chapter 1) Mr. Telo12 (Chapter 2), Alta Rica (Chapter 3), Polyspace® (Chapter 4), Escher Verification Studio Perfect Developer (Chapter 5) and the B method (Chapters 6 and 7).

The first book is dedicated to the presentation of different formal methods, such as the B method (Chapters 2 and 3), SCADE (Chapters 6 and 7) MATHLAB/ SIMULINK (Chapters 4 and 5) and Control Build13 (Chapter 8).

[Bou 12d] involves industrial examples of implementation of formal techniques based on static analysis such as abstract interpretation; examples of the use of ASTREE (Chapters 2 and 3), CAVEAT (Chapter 3), CODEPEER (Chapter 6), Frama-C (Chapters 8 and 7), and Polyspace® (Chapters 4 and 5) tools.

I thank all the manufacturers who have taken the time to redraftand improve upon these chapters.

Bibliography

[ABR 96] ABRIAL J.R., The B-Book — Assigning Programs to Meanings, Cambridge University Press, Cambridge, August 1996.

[ANS 83] ANSI, Norme ANSI/MIL-STD-1815A-1983, Langage de programmation Ada, 1983.

[ARA 97] ARAGO, “Applications des méthodes formelles au logiciel”, Observatoire français des techniques avancées (OFTA), vol. 20, Masson, Paris, June 1997.

[BAI 08] BAIER C., KATOEN J.-P., Principles of Model Checking, The MIT Press, Cambridge, MA, 2008.

[BAR 03] BARNES J., High Integrity Software: The SPARK Approach to Safety and Security, Addison Wesley, Boston, 2003.

[BOU 11] BOULANGER J.-L. (ed.), Utilisations industrielles des techniques formelles — interprétation abstraite, Hermes Lavoisier, Paris, 2011.

[BOU 12a] BOULANGER J.-L. (ed.), Techniques industrielles de modélisation formelle pour le transport, Hermes Lavoisier, Paris, 2012.

[BOU 12b] BOULANGER J.-L. (ed.), Mise en oeuvre de la méthode B, Hermes Lavoisier, Paris, forthcoming 2012.

[BOU 12c] BOULANGER J.-L. (ed.), Static Analysis of Software: the Abstract Interpretation, ISTE LTD, London and John Wiley and Sons, New York, 2012.

[BOU 12d] BOULANGER J.-L. (ed.), Formal Methods, Industrial Use from Model to the Code, ISTE LTD, London and John Wiley and Sons, New York, 2012.

[BOW 95] BOWEN J.P., HINCHEY H.G., Applications of Formal Methods, Prentice Hall, Upper Saddle River, 1995.

[COU 00] COUSOT P., Interprétation abstraite, Technique et science informatiques, vol. 19, no. 1-3, p. 155-164, Hermes, Paris, 2000.

[DIJ 75] DIJKSTRA E.W., “Guarded commands, non-determinacy and formal derivation of programs”, Communications of the ACM, vol.18, no. 8, p.453-457, August 1975.

[DIJ 76] DIJKSTRA E.W., A Discipline of Programming, Prentice Hall, Upper Saddle River, 1976.

[DOR 08] DORMOY F.-X., “Scade 6 a model based solution for safety critical software development”, Embedded Real-Time Systems Conference, 2008.

[HAD 06] HADDAD S., KORDON F., PETRUCCI L. (eds), Méthodes formelles pour les systèmes répartis et coopératifs, Hermes Lavoisier, Paris, 2006.

[HAL 91] HALBWACHS N., CASPI P., RAYMOND P., PILAUD D., “The synchronous dataflow programming language Lustre”, Proceedings of the IEEE, vol. 79, no. 9, p. 1305-1320, September 1991.

[HOA 69] HOARE CAR, “An axiomatic basis for computer programming”, Communications of the ACM, vol. 12, no. 10, p. 576-580-583, 1969.

[ISO 99] ISO/IEC 9899:1999, Programming languages — C, 1999.

[JON 90] JONES C.B., Systematic Software Development using VDM, Prentice Hall International, Upper Saddle River, 1990.

[MON 00] MONIN J.-F., Introduction aux méthodes formelles, Hermes, Paris, 2000.

[MON 02] MONIN J.-F., Understanding Formal Methods, Springer Verlag, New York, 2002.

[SPI 89] SPIVEY J.-M., The Z notation — a Reference Manual, Prentice Hall International, Upper Saddle River, 1989.

aIntroduction written by Jean-Louis BOULANGER.

1 The SCADE development environment is marketed by the company Esterel Technologies; to find out more, visit www.esterel-technologies.com.

2 To find out more about the CLEARSY company and Atelier B, visit www.clearsy.com.

3 The B-Toolkit was distributed by B-Core (UK) Ltd.

4 Atelier B and associated information can be obtained from www.atelierb.eu/.

5 For more information on Polyspace®, visit www.mathworks.com/polyspace®.

6 To find out more about Caveat, visit www-list.cea.fr/labos/fr/LSL/caveat/index.html.

7 To find out more about Absint, visit www.absint.com.

8 To find out more, visit http://frama-c.com/.

9 To find out more about ASTREE, visit www.astree.ens.fr.

10 The site www.altran-praxis.com/spark.aspx offers further information about SPARK Ada technology.

11 It should be noted that SCADE was initially a development environment basing itself on the LUSTRE language and that since version 6, SCADE has become an entirely separate language (the code generator for version 6 takes most of its input from a SCADE model, and not a LUSTRE code).

12 To find out more about MaTeLo, visit www.all4tec.net/index.php/All4tec/mateloproduct.html.

13 To find out more about the ControlBuild tool, visit www.geensoft.com/en/article/controlbuild.

Chapter 1 SPARK A Language and Tool-Set for High-Integrity Software Developmenta

1.1. Introduction

SPARK1 is used worldwide and across a range of industry sectors for the cost-effective development and assurance of high-integrity software. In this chapter, we will consider the SPARK language and the tools that support its use in increasingly large-scale, high-integrity industrial applications.

The material of this chapter is divided into three main parts, as follows:

first we present an overview of what SPARK is, including its founding principles, with simple examples;

next, we provide descriptions of a range of industrial applications of SPARK spanning more than 15 years of use, and supported by some statistics on the size of programs tackled and results achieved, again providing some illustrative material where it is possible to do so;

we finish with some conclusions drawn from the examples and applications that we have discussed, and a discussion of what is in the pipeline for future enhancements to SPARK and its support tools.

1.2. An overview of SPARK

1.2.1. What is SPARK?

SPARK is a high-level, high-integrity software development language, supported by powerful tools. The compilable elements of SPARK are a subset of Ada, but SPARK is not just a subset of Ada; an integral part of the language is its annotation language, which forms an essential part of the contractual specification of SPARK programs.

One element of a programs contract, in both Ada and SPARK is its signature: its name, arguments (together with their types and modes) and description (in accompanying comments). SPARK programs have additional contractual elements, however. These additional elements consist of a set of core annotations, which may also be supplemented by more specific proof annotations. The core annotations allow a fast, polynomial time analysis of SPARK source code to check for data-flow and information-flow errors, which can indicate a failure of the code to meet its contract. The proof annotations are optional; when these are used, they can support the mathematical proof of properties of the source code. The proofs performed can range from proof of exception freedom, at its simplest, all the way to a proof of correctness against a formal specification. The relationship of SPARK, with its additional annotations, to the full Ada language is illustrated in the following .