Boulanger - Static Analysis of Software: the Abstract Interpretation

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 : interprtationabstraite 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 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.14--dc23

2011039611

British Library Cataloguing-in-Publication Data
A CIP record for this book is available from the British Library
ISBN: 978-1-84821-320-3

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.

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 Ada 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.

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+ (SCADEs 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 Astre () 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.

the fourth volume is dedicated to the presentation of the railway sectors 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.

[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., Interprtation abstraite, Technique et Science Informatique, vol. 19, p. 155164, no. 1-2-3, Herms, Paris, 2000.

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

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