IEC 61508 in a Nutshell: An Introduction to Functional Safety

Get Complete Project Material File(s) Now! »

Formal Verification

Formal verification is a mathematical technique to prove or disprove a given specification property against a model of the system. Being exhaustive in nature, formal verification locates errors that may have been undiscovered by validation techniques (e.g., testing or simulation). While a range of techniques exists for formal verification of software, we shall discuss model checking [64], which allows automatic verification of system models against temporal specifications.

Model Checking

Model checking is an automated technique for verifying system models. The verification process explores all possible execution paths to discover execution traces that do not satisfy the given specification. Such an execution trace is referred to as counter-example and can be extracted to significantly reduce the debugging time. Due to its ease of application, model checking is often suggested to become part of the development lifecycle, especially for the development of mission critical systems.

Formal Verification

model itself may be used for the verification process, thus providing seamless integration. Since model checking is considered only as good as the model itself, this also enhances the confidence in verification results against the actual deployed system. Another crucial aspect to model checking is the specification being verified, which is most commonly provided using temporal logic. For a given model M and a system property ϕ, the notation M  ϕ is used to denote that the model satisfies the property. Conversely, we use the notation M 2 ϕ to express that the model does not hold the given property.

Temporal Logic

Starting from the initial state as the root node a system under execution may take several possible execution paths, which forms an execution tree. Temporal logic is a genre of notations that specify branching and linear behaviours of such system execution trees i.e., we can specify desirable and undesirable paths. Linear-time temporal logic (LTL) and computation tree logic (CTL) [65] are the well-known temporal logic notations for linear and branching time reasoning respectively. The expressiveness of the notations does overlap but does not completely coincide. For example in LTL it is not always possible to express requirement of the existence of a specific path that satisfies a specific sub-property. Similarly in CTL it is not always possible to express universal behaviours over a range of paths. This problem is resolved by combining the expressiveness of the two notations into a superset notation called CTL*. Using this notation, both linear and branching behaviours can be specified. An example CTL* property from the boiler control system is presented in Equation 2.5.1 namely, “On all paths, pressure relief will not be performed until the pressure exceeds the threshold value, and a path will exist where pressure relief can be enabled”.

Safety and Liveness Properties

System properties can be divided into two general categories i.e., safety and liveness [66]. Safety properties model the global absence of undesirable occurrence, for example, “something bad” must never occur in a system during the course of its execution. Whereas the liveness properties model the global presence of desirable occurrences, for example, “something good” will happen eventually. A safety property from the boiler control system is, “when the pressure exceeds a threshold, the pressure-relief control valve will always be opened”. Similarly liveness property from the boiler system is, “pressure relief valve will be closed most of the time i.e., to perform useful boiler operation”.

Probabilistic Verification

Formal verification through model checking verifies system for systematic errors that can always be avoided through design improvements and error correction. However, random failures often cannot be completely eliminated, for example, due to manufacturing defects in hardware components. Therefore applying qualitative model checking will always yield a negative result indicating the reachability of undesired execution paths. Probabilistic verification analyses less-than-perfect models, where system properties are quantitative in nature. For example in the boiler system, model checking can be used to verify the correct operation of the controller software, but the overall boiler system model also contains random failures due to hardware component failure rates. Therefore, such systems must be verified using probabilistic model checking that is, to verify that the system will work correctly with a high reliability. As presented earlier, a failure rate can be converted to an equivalent probability of failure by using a probability distribution, such as Poisson distribution (see Section 2.4.1). These probabilities are then used as annotations for the various behaviours on the system model. A probabilistic specification is then used to calculate the probability of the overall system model satisfying desirable outcomes. A probabilistic specification from the boiler system is presented as following i.e., “what is the probability of failing to open the relief valve when needed”.

Recap

So far in this chapter, we presented some basic concepts about failures, safety, system reliability and verification. These concepts are important for understanding the proposed model based safety assessment (MBSA) approach presented in Chapter 6, as well as the existing approaches. In the subsequent sections, we discuss some of the existing approaches for MBSA and provide a critical comparison with the proposed approach. We further provided a classification approach and describe some of the similarities and differences between them.

Related Work

In this section, we present a range of existing approaches for model-based safety assessment (MBSA) and classify them by their defining characteristics. Among these techniques, we narrow the focus of our survey to exclude those approaches that are not applicable to functional safety standards (e.g., IEC 61508). For example, we exclude software reliability modelling [67] techniques since IEC 61508 consider reliability models only for random errors in the hardware. Software errors are considered systematic in nature are dealt with avoidance measures such as using validation techniques on software specification, design and source code. Furthermore, we also excluded techniques that only perform qualitative analyses (e.g., [68]), as they do not address random errors in E/E/PE systems induced from hardware component failures.

Classification

Lisagor et al. [46] present a basis for classification of the existing MBSA approaches. The most important aspect of this classification is the engineering semantics for the modelling failures and nominal behaviours. This leads to the following categories.
Failure effect modelling (FEM) that is, modelling the effects of failure on the nominal behaviour of the system model, for example, the stuck at failure pattern can be modelled by disabling the potential to change in the corresponding model component.
Failure logic modelling (FLM) that is, modelling the conditions that induce the actual failure e.g., current overflow, pressure overload, or temperature overrun scenarios. These scenarios are considered beyond the nominal behaviours of the system and therefore, are often difficult to model. Furthermore, in a component-based design paradigm, the reuseability of the component should also be applied with additional care since, two similar components may fail under different circumstances.
– Hybrid failure modelling is a combination of both of the above approaches.
– Another criteria for categorization is the approach used to construct the system safety models.
– Among these, we find that most existing techniques fall in one of the following categories.
– Using dedicated models built for the purpose of safety assessment. Such models are free from complexities, for example, engineering semantics that may be unnecessary for the purpose of safety analysis.
– Using system development models after manually or automatically extending it with safety related information (e.g., as annotations). The main benefit of this approach is the partial utilisation of the system model, which ensure the consistency between safety assessment results and the deliverables of the development processes.
– We further inspect the syntax and structure used for representing the system model. Here, syntax and structure refer to the modelling language used for expressing the system behaviour and its constraints. Three categories can be derived from the choice of languages of the existing approaches, namely the following.
– Using an open standard for the purpose of model-based design such as AADL [69] and IEC 61499
– Using a proprietary standard of model-based development such as SCADE [70] and Simulink [71]
– Using a domain specific language that is developed for the explicit purpose of safety analysis such as AltaRica [72] and SAML [55]
Later in this section, we present a few approaches that are closely related to the proposed approach. These approaches use high-level modelling formalism for modelling system’s nominal and failure behaviour and enable quantitative risk assessment and safety assessment.

1. Introduction
1.1 Historical Perspective
1.2 Model-Driven Engineering
1.3 Contributions
1.4 Thesis Organisation
2. Background
2.1 Boiler Control System
2.2 Defects, Errors and Failures
2.3 System Reliability
2.4 Reliability Modelling and Analysis
2.5 Formal Verification
2.6 Recap
2.7 Related Work
3. IEC 61508 in a Nutshell: An Introduction to Functional Safety
3.1 Basic Concepts
3.2 Meeting Basic Requirements
3.3 Meeting Hardware Requirements
3.4 Meeting Software Requirements
3.5 Summary
3.6 Discussion
4. An Introduction to IEC 61499: Model-Based Design using Function Blocks
4.1 Distribution station
4.2 Basic function block
4.3 Composite function blocks
4.4 Service interface function blocks
4.5 System, Devices, and Resources
4.6 Execution models for Function Blocks
4.7 Discussion
5. Converting Function Blocks to Prism
5.1 The Boiler Control System
5.2 Formalisation
5.3 The Prism Language
5.4 Converting Function Blocks to Prism
5.5 Preserving the Execution Semantics
5.6 Discussion
6. Stochastic Function Blocks: Model-Based Safety of IEC 61499 Systems
6.1 Overview
6.2 Stochastic Function Blocks (SFB)
6.3 Transformation to PRISM
6.4 Preserving the Execution Semantics
6.5 Safety Analysis
6.6 Results
6.7 Discussion
7. BlokIDE: An IDE for Model-Based Design and Safety
7.1 Contributions
7.2 BlokIDE – Design and Implementation
7.3 BlokIDE and Functional Safety
7.4 Conclusion
8. Conclusion
8.1 Model-Based Safety
8.2 Function Blocks to Prism Conversion
8.3 Meeting IEC 61508-3 Requirements with BlokIDE
GET THE COMPLETE PROJECT
Model-Based Safety Assessment of Industrial Automation Systems using IEC 61499