Formal Methods

Industrial Use from Model to the Code

Jean-Louis Boulanger

• Publisher: Wiley-ISTE
• Year: 2013
• Print ISBN: 9781848213623
• eBook ISBN: 9781118614372
• Edition: 1
• Topic: Technology & Engineering
• Subtopic: Industrial Engineering
• Index: Technology & Engineering

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.

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

Table of contents

• Cover
• Title Page
• Copyright
• Introduction
• Chapter 1: From Classic Languages to Formal Methods
• Chapter 2: Formal Method in the Railway Sector the First Complex Application: SAET-METEOR
• Chapter 3: The B Method and B Tools
• Chapter 4: Model-Based Design Using Simulink — Modeling, Code Generation, Verification, and Validation
• Chapter 5: Proving Global Properties with the Aid of the SIMULINK DESIGN VERIFIER Proof Tool
• Chapter 6: SCADE: Implementation and Applications
• Chapter 7: GATeL: A V&V Platform for SCADE Models
• Chapter 8: ControlBuild, a Development Framework for Control Engineering
• Chapter 9: Conclusion
• Glossary
• List of Authors
• Index