Formal Methods Applied to Complex Systems E-Book

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

Seitenzahl: 626

Veröffentlichungsjahr: 2014

Beschreibung

This book presents real-world examples of formal techniques in an industrial context. It covers formal methods such as SCADE and/or the B Method, in various fields such as railways, aeronautics, and the automotive industry. The purpose of this book is to present a summary of experience on the use of "formal methods" (based on formal techniques such as proof, abstract interpretation and model-checking) in industrial examples of complex systems, based on the experience of people currently involved in the creation and assessment of safety critical system software. The involvement of people from within the industry allows the authors to avoid the usual confidentiality problems which can arise and thus enables them to supply new useful information (photos, architecture plans, real examples, etc.).

Leseprobe

Introduction

1 Presentation of the B Method

1.1. Introduction

1.2. The B method

1.3. Verification and validation (V&V)

1.4. Methodology

1.5. Feedback based on experience

1.6. Conclusion

1.7. Glossary

1.8. Bibliography

2 Atelier B

2.1. Introduction

2.2. Automatic refinement

2.3. Code generation

2.4. Proof and model animation

2.5. The move toward open source

2.6. Glossary

2.7. Bibliography

3 B Tools

3.1. Introduction

3.2. General principles

3.3. Atelier B

3.4. Open source tools

3.5. Conclusion

3.6. Glossary

3.7. Bibliography

4 The B Method at Siemens

4.1. Introduction

4.2. The development process using B

4.3. Monitoring

4.4. Digging deeper

4.5. Automatic refinement

4.6. Conclusion

4.7. Glossary

4.8. Bibliography

5 Industrial Applications for Modeling with the B Method

5.1. Introduction

5.2. Control-command systems for controlling platform doors

5.3. Safety of microelectronic components

5.4. Conclusion

5.5. Glossary

5.6. Bibliography

6 Formalization of Digital Circuits Using the B Method

6.1. Introduction

6.2. B method and VHDL

6.3. Modeling digital circuits

6.4. VHDL libraries

6.5. VHDL to B

6.6. Conclusions

6.7. Bibliography

7 Pragmatic Use of B: The Power of Formal Methods without the Bulk

7.1. Introduction

7.2. Prototyping for formal models

7.3. Inspiration from agile methods

7.4. Simultaneous development and validation

7.5. Performances of software developed in B

7.6. Use of infinity: separating algorithmic thinking and programming issues

7.7. Industrial implementation of event-B

7.8. B method for software and event-B

7.9. Conclusion

7.10. Glossary

7.11. Bibliography

8 BRILLANT/BCaml — A Free Tools Platform for the B Method

8.1. What is BRILLANT/BCaml?

8.2. Organization

8.3. Functions

8.4. Perspectives

8.5. Bibliography

9 Translating B and Event-B Machines to Java and JML

9.1. Introduction

9.2. Background

9.3. Translating B to JML

9.4. Translating Event-B to JML and Java

9.5. Future work and conclusion

9.6. Bibliography

10 Event B

10.1. Introduction

10.2. Modeling and verification of a system

10.3. Event B: a modeling language

10.4. Formal development of a sequential algorithm

10.5. Development of a distributed algorithm

10.6. Tools

10.7. Conclusion and perspectives

10.8. Bibliography

11 B-RAIL: UML to B Transformation in Modeling a Level Crossing

11.1. Introduction

11.2. Level crossings: general overview

11.3. Managing requirements

11.4. UML notation and the B method

11.5. Step 1: requirement acquisition

11.6. Step 2: environment and risk analysis

11.7. Step 3: component breakdown

11.8. Step 4: verification

11.9. UML2B

11.10. Conclusions

11.11. Glossary

11.12. Bibliography

12 Feasibility of the Use of Formal Methods for Manufacturing Systems

12.1. Introduction

12.2. Presentation of the requirement

12.3. The methods chosen and a brief description of them

12.4. Description of the machine: mechanical press with clutch-brake

12.5. Process followed for the design, validation and generation of the software using the B method

12.6. Formalization of the requirements and properties helping SysML and verification of the unitary modules by model checker

12.7. Conclusion on the use of formal techniques in the field of manufacturing

12.8. Glossary

12.9. Bibliography

13 B Extended to Floating-Point Numbers: Is it Sufficient for Proving Avionics Software?

13.1. Introduction

13.2. Motivation

13.3. Integers and the railway origins of the B method

13.4. The avionics context: floating-point numbers and complexity

13.5. Barking up the wrong tree: separation between integer and floating-point calculations

13.6. IEEE 754 Floating-point numbers

13.7. Reasons underlying extension to floating-point numbers

13.8. Returning to the useful properties that need to be proved

13.9. Conclusion

13.10. Appendix: the confusion between overflow, infinity and illegal parameters

13.11. Glossary

13.12. Bibliography

14 From Animation to Data Validation: The ProB Constraint Solver 10 Years On

14.1. The problem

14.2. Choice of implementation technology

14.3. Implementation of the PROB constraint solver

14.4. Added value of constraint programming

14.5. Acknowledgments

14.6. Bibliography

15 Unified Train Driving Policy

15.1. Introduction

15.2. Overview

15.3. Semantics

15.4. Modeling notation

15.5. Verification

15.6. Discussion

15.7. Conclusions

15.8. Bibliography

Conclusion

C.1. Introduction

C.2. B Method

C.3. Conclusion

C.4. Bibliography

Glossary

List of Authors

Index

First published 2014 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 2014 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 Control Number: 2014939764

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

Introduction

I.1. Context

Although formal program analysis techniques have a long history (including the work by Hoare [HOA 69] and Dijkstra [DIJ 75]), formal methods were only established in the 1980s. These techniques are used to analyze the behavior of software applications written using a programming language. The correctness of a program (correct behavior, program completion, etc.) is then demonstrated using a program proof based on the calculation of the weakest precondition [DIJ 76].

The application of formal methods (Z [SPI 89], VDM [JON 90] and the B method [ABR 96, ARA 97]) for industrial applications and their suitability for use in industrial contexts dates back to the late 1990s. Formal specifications use mathematical notations to give a precise description of system requirements.

Note 1.– Z – A Z specification is made up of schematic diagrams and sets used to specify a computer system. A specification is a set of schematic diagrams.

Note 2.– The Vienna Development Method (VDM) – this is a formal method based on a denotational and operational vision (programs are seen as mathematical functions), unlike Z or the B method which are based on axiomatic set theory.

One stumbling block is the possibility of implementation within the context of industrial applications (on a large scale, with cost and time constraints, etc.); this implementation requires tools to have attained a sufficient level of maturity and performance.

Note that for critical applications, at least two formal methods make use of recognized and widely available design environments covering part of the code specification process while implementing one or more verification processes: the B method [ABR 96], the LUSTRE language [HAL 91, ARA 97] and its graphic version SCADE1 [DOR 08]. The B method and the SCADE environment have been used successfully in industrial tools.

To give an example, Atelier B, marketed and sold by CLEARSY2, is a tool which covers the whole development cycle involved in the B method (specification, refining, code generation and proof). Note that Atelier B3 can be freely downloaded since version 4.0.

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

Although formal methods are now becoming increasingly widely used, they are still relatively marginal when viewed in terms of the number of lines of code involved. To date, far more lines of ADA [ANS 83], C [ISO 99] and C++ code have been produced manually than through the use of a formalr ocess.

For this reason, other formal techniques have been implemented in order to verify the behavior of software applications written in languages such as C and ADA. The main technique, abstract program interpretation, is used to evaluate all the behaviors of a software application by static analysis. In recent years, this type of technique has been applied to a number of tools, including POLYSPACE4, Caveat5, Absint6, FramaC7 and ASTREE8.

The effectiveness of these static program analysis techniques has greatly improved with increases in the processing power of personal computers. Note that these techniques generally require the insertion of additional information, such as preconditions, invariants and/or postconditions, into the manual code.

SPARK Ada9 is an approach in which the ADA language [ANS 83] has been extended [BAR 03] to include these additional tools and a suite of tailored tools has been created.

I.2. Aims of this book

[BOW 95] and [ARA 97] provided the first feedback from industrial actors concerning the use of formal techniques, notably the B method [ABR 96], the LUSTRE language [HAL 91, ARA 97] and SAO+, the precursor of SCADE10 [DOR 08]. Other works, including [MON 00, MON 02 and HAD 06], give an overview of formal methods from a more academic perspective.

Our aim in this book is to present real-world examples of the use of formal techniques.

For our purposes, the term “formal techniques” is taken to mean the different mathematically based approaches used to demonstrate that a software application respects a certain number of properties.

Note that the standard use of formal techniques consists of producing specification and/or design models, but that formal techniques are increasingly seen as tools for verification (static code analysis, to demonstrate that properties are respected, to demonstrate good management of floating points, etc.).

This book is the fifth and final volume in a series covering different aspects:

– Volume 1 [BOU 11] concerns examples of industrial implementation of formal techniques based on static analysis, such as abstract interpretation, and includes examples of the use of ASTREE, CAVEAT, CODEPEER, FramaC and POLSYPACE.

– Volume 2 [BOU 12b] presents different formal modeling techniques used in the field of rail transport, such as the B method, SCADE, Simulink DV, GaTel and Control Build and other techniques.

– Volume 3 [BOU 12a] presents different tools used in formal verification: SPARK ADA, MaTeLo, AltaRica, Polyspace, Escher and B-event.

– Volume 4 [BOU 14] gives examples of the industrial implementation of the B method [ABR 96], SCADE, and verification using Prover Verifier. Note that this volume (which presents examples of application using the B method) constitutes a useful addition to university textbooks such as [LAN 96], [WOR 96] and [SCH 01].

I wish to thank all the industrial actors who have freely given of their time to contribute such interesting and informative chapters to this book.

I.3. 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), Masson, vol. 20, June 1997.

[BAI 08] Baier C., Katoen J.-P., Principles of Model Checking, MIT Press, 2008.

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

[BOU 11] Boulanger J.-L. (ed.), Static Analysis of Software, ISTE, London, and John Wiley & Sons, New York, 2011.

[BOU 12a] Boulanger J.-L. (ed.), Industrial Use of Formal Method: Formal Verification, ISTE, London, and John Wiley & Sons, New York, 2012.

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

[BOU 14] Boulanger J.-L. (ed.), Formal Method, Applied to Industrial Complex Systems, ISTE, London, and John Wiley & Sons, New York, 2014.

[BOW 95] Bowen J.P., Hinchey M.G., Applications of Formal Methods, Prentice Hall, 1995.

[COU 00] Cousot P., “Interprétation abstraite”, Technique et Science Informatique, vol. 19, no. 1–3, pp. 155–164, January 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, August 1975.

[DIJ 76] Dijkstra E.W., A Discipline of Programming, Prentice Hall, 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, Collection IC2, Hermes, 2006.

[HAL 91] Halbwachs N., Paul C., Pascal R., et al., “The synchronous dataflow programming language Lustre”, Proceedings of the IEEE, vol. 79, no. 9, pp. 1305–1320, September 1991.

[HOA 69] Hoare C.A.R., “An axiomatic basis for computer programming”, Communications of the ACM, vol. 12, no. 10, pp. 576–580, 583, 1969.

[JON 90] Jones C.B., Systematic Software Development Using VDM, 2nd ed., Prentice Hall International, 1990.

[LAN 96] Lano K., The B Language and Method: A Guide to Practical Formal Development, Springer Verlag London Ltd., 1996.

[MON 00] Monin J.-F., Introduction aux Méthodes Formelles, Hermès, 2000. [Foreword by G. Huet]

[MON 02] Monin J.-F., Understanding Formal Methods, Springer Verlag, 2002. [Foreword by G. Huet, Translation edited by M. Hinchey]

[SCH 01] Schneider S., The B-Method: An Introduction, Palgrave, 2001.

[SPI 89] Spivey J.M., The Z Notation: A Reference Manual, Prentice Hall International, 1989.

[WOR 96] Wordsworth J., Software Engineering with B, Addison-Wesley, 1996.

Introduction written by Jean-Louis Boulanger.

1 The SCADE development environment is marketed by ESTEREL-Technologies – see http://www.esterel-technologies.com/.

2 For more information on CLEARSY and Atelier B, see http://www.clearsy.com/.

3 Atelier B and the associated information may be obtained at http://www.atelierb.eu/.

4 See http://www.mathworks.com/products/polyspace/ for further information concerning Polyspace.

5 See http://www-list.cea.fr/labos/fr/LSL/caveat/index.html for further information concerning Caveat.

6 See http://www.absint.com/ for further information concerning Absint.

7 Further details may be found at http://frama-c.com/.

8 See http://www.astree.ens.fr/ for further information concerning ASTREE.

9 The Website http://www.altran-praxis.com/spark.aspx offers additional information concerning SPARK Ada technology.

10 Note that SCADE started out as a development environment using the LUSTRE language before becoming a language in its own right from version 6 onward (the code generator for version 6 uses a SCADE model instead of a LUSTRE code as input).

1

Presentation of the B Method

1.1. Introduction

The use of formal methods [BEH 93, ARA 97, HIN 95, MON 00, BOU 11, BOU 12a, BOU 12b] is increasing, especially in critical applications such as nuclear power plants, avionics and rail transport. Ensuring maximum safety while operating an application is a significant challenge.

The contribution of formal methods is that they present a mathematical framework for the development process, which provides a method for producing software that is correct by construction. This is because the development process can be verified by validation techniques such as proof or exploration of the model.

Figure 1.1.Example of a Z diagram1

Of course, to achieve this we need a precise description of the properties that the computerized system must possess. There are different classes of formal methods: algebraic specifications (PLUSS or PVS), equational specifications (LUSTRE [HAL 91, ARA 97]) and model-oriented specifications (B [ABR 96], the Vienna Development Method (VDM) [JON 90] or Z [SPI 89]).

In contrast to model exploration-oriented validation (model-checking [BAI 08]) such as LUSTRE, the B method [ABR 96] is based on the proof of a proof obligation (or PO in the following) which guarantees the feasibility and the coherence of the model (validity of the refinement).

In the French railway industry, the use of formal methods [BEH 93, ARA 97, DEB 94, BOU 11, BOU 12a, BOU 12b], and in particular the B method, is increasingly common within the development of critical systems.

The software for these safety systems (rail signaling, automatic driving, etc.) must meet very strict quality, reliability, safety and robustness criteria.

One of the first applications of formal methods was made a posteriori on the SACEM2 [GUI 90]. During the installation of the SACEM [GEO 90], the RATP3 had carried out a Hoare proof [HOA 69] to demonstrate that the requirements had been taken into account; for more information, see [GUI 90]. The Hoare proof makes it possible to clearly show all of the postconditions, using a program P and a set of preconditions C.

The Hoare proof, which was carried out within the SACEM, showed a certain number of code properties, but it was not possible to link these with requirements related to safety (e.g. requirement for non-collision).

As a result, the decision was made to create a formal model in Z [SPI 89, DIL 95]. This formal model made it possible to break the properties down and to link the requirements with the code. Around 20 significant anomalies were discovered in this way by the team of experts responsible for the respecification in Z.

Projects such as the CTDC, KVS or the SAET-METEOR4 [BEH 93, BEH 96, BEH 97, BOU 06], LST [DEH 94], CdG VAL (VAL for Véhicule Automatique Léger – Light Automatic Vehicle)5 and the automation of Line 1 of the Parisian metro use the B method throughout the development process (from the specifications to the code).

1.2. The B method

1.2.1. Presentation

The B method was developed by Jean-Raymond Abrial6 [ABR 96], and is a formal, model-oriented method like Z [SPI 89] and VDM [JON 90]. However, unlike these methods, it also allows incremental development of the specification up to the code through the concept of refinement [MOR 90], and this is through a unique formalism: the language of abstract machines.

Figure 1.2.The “Hello” program in B

At each stage of B development, proof obligations (POs) are generated in order to guarantee the validity of the refinement and the consistency of the abstract machine. In this way, the B method makes it possible to develop safe software.

Like Z, the B method is based on set theory and first-order predicate logic. However, unlike Z, the B method has a development flavor in its way of specifying operations. In fact, operations are not specified in terms of pre- and postconditions, but by means of generalized substitutions.

In Figure 1.2, we introduce the specification of the HelloWorld program and its implementation HelloWorld_n.

1.2.2. The concept of an abstract machine

1.2.2.1. Abstract machine

A B-model is designed through composition, decomposition and refinement of abstract machines. The basic component of the B method is the abstract machine, which can be a high-level machine or a refinement of another machine. The final refinement may also be called the implementation.

The concept of an abstract machine is similar to the concept of a module and/or object, which is found in more traditional programming languages. The keyword here is “encapsulation”: the state evolution of an abstract machine should only take place through the behavior of the encapsulation.