Static Analysis of Software E-Book

• Herausgeber: John Wiley & Sons
• Kategorie: Wissenschaft und neue Technologien
• Sprache: Englisch

Seitenzahl: 446

Veröffentlichungsjahr: 2013

Beschreibung

The existing literature currently available to students and researchers is very general, covering only the formal techniques of static analysis. This book presents real examples of the formal techniques called "abstract interpretation" currently being used in various industrial fields: railway, aeronautics, space, automotive, etc. The purpose of this book is to present students and researchers, in a single book, with the wealth of experience of people who are intrinsically involved in the realization and evaluation of software-based safety critical systems. As the authors are people currently working within the industry, the usual problems of confidentiality, which can occur with other books, is not an issue and so makes it possible to supply new useful information (photos, architectural plans, real examples).

Leseprobe

Table of Contents

Introduction

Chapter 1. Formal Techniques for Verification and Validation

1.1. Introduction

1.2. Realization of a software application

1.3. Characteristics of a software application

1.4. Realization cycle

1.5. Techniques, methods and practices

1.6. New issues with verification and validation

1.7. Conclusion

1.8. Bibliography

Chapter 2. Airbus: Formal Verification in Avionics

2.1. Industrial context

2.2. Two methods for formal verification

2.3. Four formal verification tools

2.4. Examples of industrial use

2.6. Bibliography

Chapter 3. Polyspace

3.1. Overview

3.2. Introduction to software quality and verification procedures

3.3. Static analysis

3.4. Dynamic tests

3.5. Abstract interpretation

3.6. Code verification

3.7. Robustness verification or contextual verification

3.8. Examples of Polyspace® results

3.9. Carrying out a code verification with Polyspace

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

3.11. Carrying out certification with Polyspace®

3.12. The creation of critical onboard software

3.13. Concrete uses of Polyspace®

3.14. Conclusion

3.15. Bibliography

Chapter 4. Software Robustness with Regards to Dysfunctional Values from Static Analysis

4.1. Introduction

4.2. Normative context

4.3. Elaboration of the proof of the robustness method

4.4. General description of the method

4.5. Computation of the control required

4.6. Verification of the effective control of an industrial application

4.7. Discussion and viewpoints

4.8. Conclusion

4.9. Bibliography

Chapter 5. CodePeer — Beyond Bug-finding with Static Analysis

5.1. Positioning of CodePeer

5.2. A tour of CodePeer capabilities

5.3. CodePeer’s inner working

5.4. Conclusions

5.5. Bibiliography

Chapter 6. Formal Methods and Compliance to the DO-178C/ED-12C Standard in Aeronautics

6.1. Introduction

6.2. Principles of the DO-178/ED-12 standard

6.3. Verification process

6.4. The formal methods technical supplement

6.5. LLR verification by model-checking

6.6. Contribution to the verification of robustness properties with Frama-C

6.7. Static analysis and preservation of properties

6.8. Conclusion and perspectives

6.9. Appendices

6.10. Acknowledgements

6.11. Bibliography

Chapter 7. Efficient Method Developed by Thales for Safety Evaluation of Real-to-Integer Discretization and Overflows in SIL4 Software

7.1. Introduction

7.2. Discretization errors in the embedded code production chain

7.3. Modeling of the creation and propagation of uncertainties

7.4. Good practice of an analysis of real-to-integer discretization

7.5. Arithmetic overflow and division by zero

7.6. Application to a rail signalling example

7.7. Conclusion

7.8. Annexe: proof supplements

7.9. Bibliography

First published 2012 in Great Britain and the United States by ISTE Ltd and John Wiley & Sons, Inc. Adapted and updated from Utilisationsindustrielles des techniques formelles : interprétationabstraite published 2011 in France by Hermes Science/Lavoisier © LAVOISIER 2011

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 27-37 St George’s Road London SW19 4EU UK

www.iste.co.uk

John Wiley & Sons, Inc. 111 River Street Hoboken, NJ 07030 USA

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

Static analysis of software : the abstract interpretation / edited by Jean-Louis Boulanger. p. cm. Includes bibliographical references and index.   ISBN 978-1-84821-320-3   1. Computer software--Testing. 2. Debugging in computer science. 3. Computer software--Quality control. I. Boulanger, Jean-Louis.   QA76.76.T48S75 2011   005.1′4--dc23

2011039611

British Library Cataloguing-in-Publication Data

Introduction1

Context

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

It was not until the end of the 1990s that formal methods (Z [SPI 89], VDM [JON 90]) and the B method [ABR 96, ARA 97] were used in industrial applications and could be applied in an industrial context. One of the obstacles to their use was how they could be implemented in an industrial application (large application, time and cost constraints, etc.). They could only be implemented using tools that were mature enough and had sufficient performance.

It is worth noting that in the context of critical applications, at least two formal methods have a recognized and commonly used design environment that covers part of the realization of the code specification process while integrating one or several verification processes, that is to say the B method [ABR 96] and Lustre language [HAL 91, ARA 97] and its graphic version, called SCADE® [DOR 08]. The B method and SCADE® environment are associated with proven industrial tools. For example, AtelierB and Btoolkit, commercially produced by Clearsy and Bcore, respectively, are tools that completely cover the B method development cycle (specification, refinement, code generation and proof).

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

The use of formal methods, though in full expansion, is still marginal compared to the number of code lines. Indeed, there are currently many more lines of Ada [ANS 83], C and C++ code that have been manually produced via a formal process only. For this reason 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 main technique, called abstract program interpretation [COU 00], enables us to evaluate the set of behaviors of a software application using static analysis. In the past few years, this type of technique has given rise to several tools, such as Polyspace®1, Caveat2, Absint3, Frama-C4 and/or Astrée5.

The efficiency of these static program analysis techniques has greatly progressed with the increase in the power of office equipment. It is worth noting that these techniques generally require the integration of complementary information into the manual code, such as pre-conditions, invariants and/or post-conditions.

SPARK Ada6 is an approach where Ada has been extended [BAR 03] in order to introduce additional elements (pre, post and invariant) and a sequence of adapted tools has been defined.

Objective

In [BOW 95] and [ARA 97], we have the first feedback from industrialists regarding formal techniques, and in particular feedback on the B method, Lustre language [HAL 91, ARA 97] and SAO+ (SCADE®’s predecessor). Other works, such as [MON 00, MON 02, HAD 06] provide an overview of formal methods from a scientific point of view.

With regards to the presentation of context and the state of the literature, our objective is to present concrete examples of the industrial uses of formal techniques. By formal techniques, we mean different approaches based on mathematics, which enable us to demonstrate that a software application respects a certain number of properties.

It is worth noting that the standard use of formal techniques consists of running specification and/or design models. Increasingly, however, formal techniques are seen as a way of carrying out verification (static code analysis, proof that the property is respected, proper management of floater calculation, etc.).

This book is part of a series that covers four different aspects:

– this first volume concerns industrial examples of the implementation of formal techniques based on static analysis, such as abstract interpretation: there are examples of the use of Astrée (Chapter 2), Caveat (Chapter 2), CodePeer (Chapter 5), Frama-C (Chapters 2 and 6) and Polsypace® (Chapters 3 and 4) tools;

– the second volume gives industrial examples of B method implementation [ABR 96];

– the third volume is dedicated to the presentation of different modeling techniques, such as SCADE®7 [DOR 08], ControlBuild8 and MaTeLo9.

– the fourth volume is dedicated to the presentation of the railway sector’s application of formal technics.

In conclusion to this introduction, I would like to thank all the industrialists who have given their own time to write these chapters, each one being even more interesting than the next.

Bibliography

[ABR 96] ABRIAL Jr., The B Book – Assigning Programs to Meanings, Cambridge University Press, Cambridge, August 1996.

[ANS 83] ANSI, ANSI/MIL-STD-1815A-1983 Standard, ADA Programming Language, ANSI, 1983.

[BAI 08] BAIER C., KATOEN J.P., Principles of Model Checking, MIT Press, London, 2008.

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

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

[COU 00] COUSOT P., “Interprétation abstraite”, Technique et Science Informatique, vol. 19, p. 155–164, no. 1-2-3, Hermès, Paris, 2000.

[DIJ 75] DIJKSTRA E.W., “Guarded commands, nondeterminacy and formal derivation of programs”, Communications of the ACM, vol.18, no. 8, pp. 453–457, 1975.

[DIJ 76] DIJKSTRA E.W., A Discipline of Programming, Prentice Hall, Engelwood Cliffs, 1976.

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

[HAD 06] HADDAD S. (ed.), KORDON F., PETRUCCI L., Méthodes Formelles pour les Systèmes Répartis et Coopératifs, Hermès Lavoisier, Paris, 2006.

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

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

[JON 90] JONES C.B., Systematic Software Development using VDM, (2nd edition), Prentice Hall, Engelwood Cliffs, 1990.

[MON 00] MONIN J.F., Introduction aux Méthodes Formelles, Hermès, Paris, 2000.

[MON 02] MONIN J.F., Understanding Formal Methods, Springer Verlag, Heidelberg, 2002.

[OFT 97] OBSERVATOIRE FRANÇAIS des TECHNIQUES AVANCEES (OFTA), Applications des Méthodes Formelles au Logiciel, vol. 20, Arago, Masson, Paris, June 1997.

[SPI 89] SPIVEY J.M., The Z Notation – a Reference Manual, Prentice Hall, Engelwood Cliffs, 1989.

1 Introduction written by Jean-Louis BOULANGER.

1 See www.mathworks.com/products/polyspace/.

2 See www-list.cea.fr/labos/fr/LSL/caveat/index.html.

3 See web www.absint.com.

4 To find out more, see web frama-c.com.

5 See www.astree.ens.fr.

6 See www.altran-praxis.com/spark.aspx contains additional information about SPARK Ada.

7 SCADE® is distributed by Esterel-Technologies, see www.esterel-technologies.com.

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

9 To find out more about MaTeLo, see www.all4tec.net/index.php/All4tec/matelo-product.html.

Chapter 1Formal Techniques for Verificationand Validation1

1.1. Introduction

The aim of this chapter is to recall concepts and techniques that are implemented in order to verify and validate software based systems.

Verification and validation (V&V) activities are essential if we are to build a software application that reaches a specific confidence level. V&V encompasses a set of activities that extend over the entire realization cycle.

Within this relationship, we place ourselves in the context of a process of software realization that is based on a V-cycle, as the standards applicable to dependable systems recommend (generic, CEI/IEC 61508 [IEC 98], rail, CENELEC EN 50128 [CEN 01], aeronautical, DO178 [RTA 92], nuclear [IEC 06] and automotive ISO 26262 [ISO 09]).

1.2. Realization of a software application

It is worth noting that we are talking about the realization of a software application and not the development of a software application. The realization of a software application includes development activities but also activities of verification, validation, production, installation and maintenance.

Figure 1.1.Realization of a software application

V&V activities are important and will be more or less developed depending on the required safety level. The production activities of the final application and the installation are crucial, and require the implementation of specific processes. The decommissioning of a software application is mentioned but is of no concern, in contrast to the decommissioning of a complex system, such as the decommissioning of a nuclear plant or a rail installation.

Maintenance of the software application is a very difficult activity. Indeed, after evolution it is necessary to uphold the safety level while controlling the cost of the evolution and minimizing the impact on the system in service.

A software application is faced with a problem when it comes to maintenance: its lifespan. For rail, the lifespan is 40 to 50 years, for aeronautics it is 40 years, for nuclear power 50 years and for the automotive industry it is 15 years. In view of these lifespans it is necessary to take measures in order to guarantee the maintenance of the service and the software application.

1.3. Characteristics of a software application

It is possible to characterize a software application according to the following properties:

– visible but intangible: anyone is capable of implementing a software application and identifying its behaviors but an application remains a series of bits copied into a memory, the alteration of which produces another application;

– used but does not wear out: a software application has so-called systematic faults but the wear due to time does not degrade the software application; we say that it is aging, in the sense that its performances become degraded (for example during changes in versions of the operating system), it no longer corresponds to the standard and the behaviors on the new architecture are no longer the same;