Formal Methods: Industrial Use from Model to the Code

Introduction ¹

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 CLEARSY¹ and B-Core² 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 B³ 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 POLYSPACE⁴, Caveat⁵, Absint⁶, Frama-C⁷, and/or ASTREE⁸.

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 Ada⁹ [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 SCADE¹⁰ [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 ControlBuild¹¹ (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), MaTeLo¹² (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 Methods ¹

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.

Figure 1.2. V-cycle

Description of each module/component (data, algorithms, etc.) is achieved within the framework of the design. The design phase is often separated into two stages. The first stage, named preliminary design, aims to identify manipulated data and necessary services; the second stage, named detailed design, aims to describe all services through their algorithms. The design phase then gives rise to the coding phase.

Figure 1.2 shows that there are different test phases: module tests (focused on the lowest-level components), integration tests (focused on software and/or hardware interfaces), and functional tests (sometimes known as validation tests), which show that a product conforms to its specification. As for the operation/maintenance phase, it involves operational life and control of potential evolutions.

There is a horizontal correspondence (dotted arrow) between activity specification and design and activity testing. The V-cycle is thus broken down into two phases: bottom-up phase and top-down phase. Top-down phase activity (execution of the MT/IT and FT) must be processed during the bottom-up phase. Figure 1.3 is thus closer to the V-cycle recommended.

Figure 1.3. V-cycle including test specifications

1.2.1.2. Advantages/disadvantages

The V-cycle of Figure 1.3 reveals that faults introduced in the making of the software application will be detected during the top-down phase, which has a direct impact on the cost and delays of making the software.

Experience in safety-critical applications shows that activity testing accounts for 50% to 75% of the cost of production and that the presence of faults can multiply delays in production two or three times over.

Increased delays are caused by the discovery of anomalies, their identification, analysis of their effects (impact on the safety and/or reliability of the software application), selection of anomalies to correct, analysis of anomalies, implementation of corrections and verification of corrections (in general, verifying correct implementation of modifications is achieved through test runs, but it will be necessary to verify that no additional modification has been implemented).

Analysis of anomalies is achieved through an impact analysis (definition 1.1) and a non-regression analysis (definition 1.2). In certain cases, non-regression is said to be total, and for this, it is necessary to re-execute the series of tests on one phase or all phases.

The objective of non-regression analysis is to minimize the cost of a new version.

DEFINITION 1.1.— IMPACT ANALYSIS. Impact analysis of an anomaly consists of identifying modifications to make in the bottom-up phase (impact on the documents, impact on the code, impact on the description and test implementations) of production.

DEFINITION 1.2.— NON-REGRESSION ANALYSIS. Non-regression analysis consists of determining a series of tests, which make it possible to demonstrate that the modification made has not had an effect on the rest of the software application¹.

In addition, it should be noted that the cost of correcting a fault is directly linked to the phase during which it is identified. In effect, detecting a fault during the functional testing phase is 10 to 100 times more expensive (not to mention higher in certain cases) than a fault identified in the module testing phase. This cost is linked to resources that have been used right up to discovery of the fault and to the difficulty of carrying out functional testing (usage of targeting equipment, necessity of taking real time into account, difficulty of observation, technical expertise of people involved, etc.).

Our experience feedback (in a railway system² evaluator/certifier capacity) leads us to conclude that the unitary and integration testing phases are not effective, given that manufacturers consider that:

– module testing is useless (as a general rule, module tests are defined from the code);

– software/software integration is reduced to a big-bang integration (integration of all the code in place of a module-by-module integration); at worst, all the code is compiled suddenly and integration is reduced to an interface verification by the compiler;

– software/hardware integration is supported by functional testing on a target. If all of the software is being executed correctly on the target machine, the integration is correct.

Figure 1.4. Cycle management of anomalies

Cost and delay management imply two necessities:

– N.1: reducing the number of faults introduced into the application during the bottom-up phase of the V-cycle;

– N.2: identifying faults introduced within the software application as early as possible.

1.2.2. Coding

1.2.2.1. Presentation

The classic development process of a software application is based on the use of programming language, for example Ada [ANS 83, ISO 95] C [ISO 99] and/or C++ [ISO 03].

Even if these languages have a certain abstraction level with respect to the code ultimately executed on the computer, they necessitate the writing of a line of code.

It is not possible to analyze all the current programming languages for all industries. We shall analyze the advancements that have taken place in the rail sector.

1.2.2.2. Assessment

1.2.2.2.1. The Ada language

The first rail applications in France were programmed in the middle of the 1980s with the Modula 2 language. Since then however, the Ada 83 language [ANS 83] has become the reference language for the development of safety-critical applications [RIC 94].

As Table 1.1 shows, in the context of applications that have a high level of criticality (SSIL3/SSIL4), the Ada language is only R (recommended); it is necessary to establish a sub-assembly of the language so that use of Ada be HR (highly recommended).

Table 1.1. CENELEC EN 50128 [CEN 01] — Table A.15

Ada was designed on the initiative of the DoD (the US Department of Defense) to federate more than 400 languages or dialects used by this body since the 1970s.

Ada is very widely used in the framework of embedded software applications in avionics (airbus), the space (the Ariane rocket), and the rail sector. The principal characteristic of these systems is that they require a correction of the execution.

The Ada 83 language [ANS 83] has advanced toward a second major standard, Ada 95 [ISO 95], which is the first object-normalized language. It provides the possibility of constructing object-oriented models. The latest version to date is called Ada 2005.

Figure 1.5. Example of Ada code

DEFINITION 1.3.— CERTIFICATION. Certification consists of achieving a certificate, which is a commitment that the product complies with a normative referential. Certification is based on the results of an evaluation and on production of a certificate.

Regarding certification (see definition 1.3) of Ada compilers, the existence of a standard and of a semantic of Ada has made it possible to define a compiler certification process.

This process has been implemented on different compilers and is based on a suite of tests named ACATS (Ada Conformity Assessment Test Suite); see the [ISO 99a] standard. To find out more, consult [ADA 01].

At present, these new versions of Ada have not been adopted by the embedded systems sector, because of their object-oriented aspect.

Given their efficacy, however, Ada 95 compilers are used for compilation provided that a sub-assembly of the language, which does not use the object-oriented features is relied upon.

John Barnes, in the context of the AdaCore article makes a presentation on the strength of the Ada 2005 language (syntax and semantics, strong typing, sound management of the pointer and the memory, etc.) and the impact of its implementation to demonstrate that the software is reliable.

The object-oriented aspect is not taken into account by the CENELEC EN 50128 ([CEN 01], DO 178 [ARI 92], CEI/IEC 61508 [IEC 98], ISO 26262 [ISO 09]) standards applicable to safety-critical applications.

To get around this stumbling block, the ISO 15942 [ISO 00] standard delineates a restriction on Ada 95 language constructions and defines some rules of use (programming style), which enable creation of a supposedly-certifiable application (see definition 1.4).

DEFINITION 1.4.– CERTIFIABLE APPLICATION. A certifiable software application is a software application that has been created to be certified.

The SPARK Ada language [BAR 03] is a programming language, which is a sub-assembly of Ada. All the complex structures of Ada regarded as risky or not allowing for an easy safety demonstration are not to be found in SPARK Ada. A mechanism enabling the addition of annotations in the code has been introduced.

SPARK Ada tools contain a compiler, but also a verifier for annotations. There is a free version of the SPARK Ada tools⁴. Chapter 1 of a future book by the same authors (to appear in 2012) will provide the opportunity to present the SPARK Ada tool as well as some industrial examples of its implementation.

1.2.2.2.2. The C language

The C⁵ language [KER 88] was one of the first languages to be made available to developers to create complex applications. The principal difficulty of C resides in the partial definition of the language, which means that different compilers generate one executable with different behaviors. It has since been subject to a standardization process by the ANSI [ISO 99].

Regarding the use of the C language [ISO 99], contingent upon the safety level required, the CENELEC EN 50128 [CEN 01] standard recommends defining a subassembly of the language (see Table 1.1), the execution of which is controllable.

Table 1.2 (an extract from the new version of the CENELEC EN 50128 [CEN 11] standard) shows that there was sufficient experience feedback for the Ada, C and C++ languages, enabling no further explicit mention of the notion of sub-assembly of the language as it is taken as established.

Figure 1.6 presents a piece of C code, which can give two different codes contingent upon anomaly (a) or (b) that is implemented.

This example emphasizes the weaknesses of the C language, small programming errors that are not detected in the compilation. It should be noted that this type of error is detected if the programming language used is Ada.

Table 1.2. New CENELEC EN 50128 [CEN 11] — Table A.15 (partial)

Certain weaknesses of C may be overcome by implementing some programming rules; by way of an example, to avoid an anomaly of the type if (a = cond) instead of if (a == cond), a rule of the following form can be implemented: in the framework of comparison with a variable, this must be in the left part of the expression.

From 1994, some experience feedback regarding the implementation of C (see for example [HAT 94]) has revealed that it was possible to define a sub-assembly of C usable to create software applications needing a high level of safety (SSIL3, SSIL4).

In fact, since the end of the 1990s, the MISRA-C [MIS 98, MIS 04] standard, which was developed by the Motor Industry Software Reliability Association (MISRA⁶), has become a standard for the C language.

Figure 1.6. Example⁷ of a fault in C

MISRA-C [MIS 04] specifies some programming rules (see the examples of Table 1.3) making it possible to avoid execution errors provoked by poorly defined constructions, unforeseen behaviors (certain C language structures are not completely defined) and misunderstandings between those people in charge of production (legible code, code with implicit cast, etc.). Several tools enable the MISRA-C rules to be automatically verified.

The MISRA-C [MIS 04] standard repeats some rules, which are explicit in several standards (see for example 14.4 and 14.7):

– rule 14.4: in the EN 50128 standard — Table A.12 or the IEC 61508 standard — Table B.1;

– rule 14.7: in the EN 50128 standard — Table A.20 or the IEC 61508 standard — Table B.9;

– etc.

MISRA-C [MIS 98] was created in 1998 and updated in 2004 [MIS 04], which shows that some experience feedback has been made use of.

Table 1.3. Some MISRA-C: 2004 [MIS 04] rules

The principal difficulty of C remains the choice of a compiler having sufficient experience feedback at its disposal for the chosen target and safety level to be achieved.

In the absence of a precise and complete standard, there is currently no certification process for C compilers, even though there are initiatives such as [LER 09]⁹.

1.2.2.2.3. Object-oriented language

As already stated, the object-oriented aspect is not taken into account by the CENELEC EN 50128 ([CEN 01], DO 178 [ARI 92], CEI/IEC 61508 [IEC 98], ISO 26262 [ISO 09]) standards applicable to safety-critical applications.

The object-oriented aspect is cited in the CENELEC EN 50128 [CEN 01] standard, but the constraints applying to languages do not allow for development of a safety-critical application (SSIL3 and SSIL4) with this type of language (see Table 1.4).

Table 1.4. CENELEC EN 50128 [CEN 01] — Table A.12

As shown by Tables 1.1 and 1.2, the C++ language [ISO 03] is cited as applicable but certain recommendations are not compatible with the use of an object-oriented language, as shown in Table 1.4.

C++ was developed during the 1980s; it proceeded from an improvement of the C language. C++ introduces the notion of class, inheritance, virtual functions, and overload. It was standardized by the ISO in 1998 and in 2003 [ISO 03].

Since the beginning of the 2000s, many attempts have been made to define a framework enabling the use of the C++ language for the development of high-safety level applications (SSIL3, SSIL4). The following works can be cited:

– JSF++ (Join Strike Fighter C++), which has published a guide [LOC 05] regarding the current work, notably the MISRA-C: 1998 [MIS 98] standard;

– MISRA, which has developed the MISRA-C++: 2008 [MIS 08] standard; Table 1.5 shows some MISRA-C++: 2008 rule examples;

– OOTIA¹⁰ (Object Oriented Technology in Aviation), which has published several guides [OOT 04a, OOT 04b, OOT 04c, OOT 04d].

Table 1.5. Some MISRA-C++: 2008 [MIS 08] rules¹²

C++ [ISO 03] is therefore quite an old language.