Formal Methods E-Book

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

Seitenzahl: 426

Veröffentlichungsjahr: 2013

Beschreibung

Although formal analysis programming techniques may be quite old, the introduction of formal methods only dates from the 1980s. These techniques enable us to analyze the behavior of a software application, described in a programming language. It took until the end of the 1990s before formal methods or the B method could be implemented in industrial applications or be usable in an industrial setting. Current literature only gives students and researchers very general overviews of formal methods. The purpose of this book is to present feedback from experience on the use of "formal methods" (such as proof and model-checking) in industrial examples within the transportation domain. This book is based on the experience of people who are currently involved in the creation and evaluation of safety critical system software. The involvement of people from within the industry allows us to avoid the usual problems of confidentiality which could arise and thus enables us to supply new useful information (photos, architecture plans, real examples, etc.). Topics covered by the chapters of this book include SAET-METEOR, the B method and B tools, model-based design using Simulink, the Simulink design verifier proof tool, the implementation and applications of SCADE (Safety Critical Application Development Environment), GATeL: A V&V Platform for SCADE models and ControlBuild. Contents 1. From Classic Languages to Formal Methods, Jean-Louis Boulanger. 2. Formal Method in the Railway Sector & #8232;the First Complex Application: SAET-METEOR, Jean-Louis Boulanger. 3. The B Method and B Tools, Jean-Louis Boulanger. 4. Model-Based Design Using Simulink - Modeling, Code Generation, Verification, and Validation, Mirko Conrad and Pieter J. Mosterman. 5. Proving Global Properties with the Aid of the SIMULINK DESIGN VERIFIER Proof Tool, Véronique Delebarre and Jean-Frédéric Etienne. 6. SCADE: Implementation and Applications, Jean-Louis Camus. 7. GATeL: A V&V Platform for SCADE Models, Bruno Marre, Benjamin Bianc, Patricia Mouy and Christophe Junke. 8. ControlBuild, a Development Framework & #8232;for Control Engineering, Franck Corbier. 9. Conclusion, Jean-Louis Boulanger.

Leseprobe

Table of Contents

Introduction

Chapter 1. From Classic Languages to Formal Methods

1.1. Introduction

1.2. Classic development

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

1.4. Formal methods

1.5. Conclusion

1.6. Bibliography

Chapter 2. Formal Method in the Railway Sector the First Complex Application: SAET-METEOR

2.1. Introduction

2.2. About SAET-METEOR

2.3. The supplier realization process

2.4. Process of verification and validation set up by RATP

2.5. Assessment of the global approach

2.6. Conclusion

2.7. Appendix

2.8. Bibliography

Chapter 3. The B Method and B Tools

3.1. Introduction

3.2. The B method

3.3. Verification and validation (V&V)

3.4. B tools

3.5. Methodology

3.6. Feedback

3.7. Conclusion

3.8. Bibliography

Chapter 4. Model-Based Design Using Simulink — Modeling, Code Generation, Verification, and Validation

4.1. Introduction

4.2. Embedded software development using Model-Based Design

4.3. Case study — an electronic throttle control system

4.4. Verification and validation of models and generated code

4.5. Compliance with safety standards

4.6. Conclusion

4.7. Bibliography

Chapter 5. Proving Global Properties with the Aid of the SIMULINK DESIGN VERIFIER Proof Tool

5.1. Introduction

5.2. Formal proof or verification method

5.3. Implementation of the SIMULINK DESIGN VERIFIER tool

5.4. Experience feedback and methodological aspects

5.5. Study case feedback and conclusions

5.6. Contributions of the methodology compared with the EN50128 normative referential

5.7. Bibliography

Chapter 6. SCADE: Implementation and Applications

6.1. Introduction

6.2. Issues of embedded safety-critical software

6.3. Origins of SCADE

6.4. The SCADE data-flow language

6.5. Conclusion: extensions of languages for controllers and iterative processing

6.6. The SCADE system

6.7. Application of SCADE in the aeronautical industry

6.8 Application of SCADE in the rail industry

6.9. Application of SCADE in the nuclear and other industries

6.10. Conclusion

6.11. Bibliography

Chapter 7. GATeL: A V&V Platform for SCADE Models

7.1. Introduction

7.2. SCADE language

7.3. GATeL prerequisites

7.4. Assistance in the design of test selection strategies

7.5. Performances

7.6. Conclusion

7.7. Bibliography

Chapter 8. ControlBuild, a Development Framework for Control Engineering

8.1. Introduction

8.2. Development of the control system

8.3. Formalisms used

8.4. Safety arrangements

8.5. Examples of railway use cases

8.6. Conclusion

8.7. Bibliography

Chapter 9. Conclusion

9.1. Introduction

9.2. Problems

9.3. Summary

9.4. Implementing formal methods

9.5. Realization of a software application

9.6. Conclusion

9.7. Bibliography

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

Formal methods : industrial use from model to the code / edited by Jean-Louis Boulanger. p. cm. -- (Industrial implementation of formal methods series) Includes bibliographical references and index. ISBN 978-1-84821-362-3 1. Railroads--Management--Data processing. 2. Formal methods (Computer science) 3. Application software--Development. I. Boulanger, Jean-Louis. TF507.F66 2012 385.0285′53--dc23

2012011496

British Library Cataloguing-in-Publication Data

Introduction1

Context

Although formal analysis programming techniques (see works by Hoare [HOA 69] and Dijkstra [DIJ 75]) are relatively old, the introduction of formal methods only dates from the 1980s. These techniques enable us to analyze the 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 used in industrial applications and settings.

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

Where safety requirements are critical, at least two formal methods are used: the B-method [ABR 96] and the LUSTRE language [HAL 91, ARA 97] and its graphic version, named SCADE [DOR 08]. These cover one part of the specification production process according to the code and integrate one or more verification processes.

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

For example, Atelier B and the B-Toolkit, marketed by CLEARSY1 and B-Core2 respectively, are tools that completely cover the development cycle proposed by the B-method comprising specification, refinement, code, and proof generation. It should be noted that Atelier B3 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 these last few years, given rise to several tools such as POLYSPACE4, Caveat5, Absint6, Frama-C7, and/or ASTREE8.

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 Ada9 [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], the first 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 SCADE10 [DOR 08]. Other works 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 mathematical approaches, which make it possible to demonstrate that a software application obeys some properties.

While the standard use of formal techniques consists of making specification and/or design models, they are seen by a verification subject to 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 12a] and [BOU 12b].

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

[BOU 12a] 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 3 and 7), and POLYSPACE (Chapters 4 and 5) tools.

[BOU 12b] is dedicated to the presentation of different formal techniques, such as the SPARK Ada (Chapter 1), MaTeLo12 (Chapter 2), AltaRica (Chapter 3), Polyspace (Chapter 4), Escher verification Studio Perfect Developer (Chapter 5) and the B method (Chapters 6 and 7).

In conclusion to this introduction, I have to thank all the manufacturers who have taken the time to redraft and 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 12a] BOULANGER J.-L. (ed.), Static Analysis of Software — The Abstract Interpretation, ISTE Ltd, London and John Wiley and Sons, New York, 2012.

[BOU 12b] BOULANGER J.-L. (ed.), Industrial Use of Formal Methods, ISTE Ltd, London, 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, Hermès, 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. (ed.), Méthodes formelles pour les systèmes répartis et coopératifs, Hermès, 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 C.A.R, “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, préface by HUET G., Hermès, Paris, 2000.

[MON 02] MONIN J.-F., Understanding Formal Methods, preface by HUET, G., TRAD. M., Hinchey, Springer Verlag, New York, 2002.

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

1 Introduction written by Jean-Louis BOULANGER.

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

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

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

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

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

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

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

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

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

10 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).

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

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

Chapter 1

From Classic Languages to Formal Methods1

1.1. Introduction

The introduction to this book has provided the opportunity to set formal analysis techniques in a general context. In this chapter, we are going to focus on formal methods and their implementation.

The classic development process of a software application is based on the use of a programming language (for example, Ada [ANS 83], C [ISO 99] and/or C++ [ISO 03]). These languages have a certain abstraction level in comparison to the code finally executed on the computer, a program is a set of line of code write manually.

The size of applications has gone from several thousands of lines to several hundreds of thousands of lines of code (possibly several millions for new applications). Considering the number of faults introduced by developers, it is then important to use techniques to limit the number of faults introduced and to more easily identify potential faults.

As we will show later, formal methods enable us to fulfill this double objective.

1.2. Classic development

The objective of this section is to analyze the weaknesses of the classic (meaning non-formal) process, which is implemented to make a software application.

1.2.1. Development process

1.2.1.1. Presentation

The creation of a software application is broken down into stages (specification, design, coding, tests, etc.). We refer to the lifecycle. The lifecycle is necessary to describe the dependencies and sequencing between activities.

Figure 1.1.Three possible lifecycles

The lifecycle must take into account the progressive refinement aspect of the development as well as possible iterations. In this section, we present the lifecycle, which is used to make a software application.

As Figure 1.1 shows, there are several cycles: a) V-cycle, b) waterfall cycle, c) spiral cycle, etc. for making a software application, but the cycle recommended by different standards (CENELEC EN 50128 [CEN 01], DO 178 [ARI 92], IEC 61508 [IEC 98], ISO 26262 [ISO 09]) remains the V-cycle.

Figure 1.2 presents the V-cycle as it is generally presented. The objective of needs analysis is to verify adequacy to the expectations of the client and technological feasibility. The objective of the specification phase is to describe what the software must do (and not how it will do it). In the context of architecture definition, the aim is create a hierarchical breakdown of the software application into modules/components and to identify interfaces between these elements.