IEC TS 61508-3-2:2024

Functional safety of electrical/electronic/programmable electronic safety-related systems - Part 3-2: Requirements and guidance in the use of mathematical and logical techniques for establishing exact properties of software and its documentation

IEC TS 61508-3-2:2024 covers the general assurance of dependable software used in critical operational-technology (OT) which is running on hardware devices which are specified as part of the OT application. It is particularly aimed at safety-related software which is being developed according to the E/E/PE software functional safety standard IEC 61508-3; in particular, the development of the software follows a Formal Safety Requirements Specification. Successful use of some or all of the assurance points specified in this document enhances the confidence that a particular piece of safety-related software meets the requirements of the SIL of the safety function which it (partially or fully) implements, and thereby increases the systematic capability of the software.

General Information

• Status: Published
• Publication Date: 25-Aug-2024
• ICS: 25.040.40 - Industrial process measurement and control
• Technical Committee: SC 65A - System aspects
• Drafting Committee: PT 61508-3-2 - TC 65/SC 65A/PT 61508-3-2
• Current Stage: PPUB - Publication issued
• Start Date: 26-Aug-2024
• Completion Date: 20-Sep-2024

Overview

IEC TS 61508-3-2:2024 is a Technical Specification in the IEC 61508 series that gives requirements and guidance for using mathematical and logical techniques (M&LT / formal methods) to establish exact properties of safety-related software and its documentation. It targets dependable software for operational-technology (OT) systems developed to a Formal Safety Requirements Specification and intended to meet a given Safety Integrity Level (SIL). The specification complements IEC 61508-3 by focusing on formal techniques that increase systematic capability and confidence that software implements its safety function correctly.

Key topics

• Scope and applicability: Use of M&LT for software running on OT hardware, aligned with IEC 61508-3 development practices.
• Assurance points: Formal triples (S1, S2, property P) where mathematical proofs can establish joint properties between software artifacts.
• Formal specifications: Guidance on producing a Formal Safety Requirements Specification, and on formal software architecture and design specifications.
• Languages and compilation: Selection of executable source-code-level (ESCL) languages, coding standards (language subsetting), and safe compilation practices including code generation.
• Verification techniques: Static analysis (e.g., abstract interpretation), automated theorem provers/automated proving, model checking and other M&LTs to prove exact properties of source and object code.
• Run-time behavior: Handling of run-time errors, exceptions and techniques for assuring absence or controlled management of runtime faults.
• Normative and informative annexes:
  • Annex A (normative): Applicable M&LTs (Table A.1).
  • Annex B (informative): Specific techniques and tools (Table B.1).
  • Annex C (informative): Properties assured by M&LTs (Table C.1).
  • Annex D (informative): Software refinement and transformation traces from specification to code.

Applications

• Safety engineers and software developers: Implement and verify safety-related software to meet SIL claims using formal proofs, static analysis and coding standards.
• Verification and validation teams: Define and check assurance points, select appropriate M&LT tools, and produce evidence for assessments.
• System integrators and OT operators: Apply formal methods to components of E/E/PE systems where increased assurance is needed.
• Assessors and certification bodies: Evaluate evidence that software meets IEC 61508-3 requirements and SIL targets through documented M&LT application.

Related standards

• IEC 61508-3:2010 - Software requirements for functional safety (normative reference).
• IEC 61508-4:2010 - Definitions and abbreviations (normative reference).
• The TS is part of the broader IEC 61508 suite for functional safety of E/E/PE systems.

This specification is essential when adopting formal methods, mathematical verification, and rigorous software assurance to strengthen confidence in safety-related OT software and to provide auditable evidence aligned with IEC functional-safety processes.

Standards Content (Sample)

IEC TS 61508-3-2 ®
Edition 1.0 2024-08
TECHNICAL
SPECIFICATION
Functional safety of electrical/electronic/programmable electronic safety-related
systems –
Part 3-2: Requirements and guidance in the use of mathematical and logical
techniques for establishing exact properties of software and its documentation

All rights reserved. Unless otherwise specified, no part of this publication may be reproduced or utilized in any form
or by any means, electronic or mechanical, including photocopying and microfilm, without permission in writing from
either IEC or IEC's member National Committee in the country of the requester. If you have any questions about IEC
copyright or have an enquiry about obtaining additional rights to this publication, please contact the address below or
your local IEC member National Committee for further information.

IEC Secretariat Tel.: [phone]
3, rue de Varembé [e-mail]
CH-1211 Geneva 20 www.iec.ch
Switzerland
About the IEC
The International Electrotechnical Commission (IEC) is the leading global organization that prepares and publishes
International Standards for all electrical, electronic and related technologies.

About IEC publications
The technical content of IEC publications is kept under constant review by the IEC. Please make sure that you have the
latest edition, a corrigendum or an amendment might have been published.

IEC publications search - webstore.iec.ch/advsearchform IEC Products & Services Portal - products.iec.ch
The advanced search enables to find IEC publications by a Discover our powerful search engine and read freely all the
variety of criteria (reference number, text, technical publications previews, graphical symbols and the glossary.
committee, …). It also gives information on projects, replaced With a subscription you will always have access to up to date
and withdrawn publications. content tailored to your needs.

IEC Just Published - webstore.iec.ch/justpublished
Electropedia - www.electropedia.org
Stay up to date on all new IEC publications. Just Published
The world's leading online dictionary on electrotechnology,
details all new publications released. Available online and once
containing more than 22 500 terminological entries in English
a month by email.
and French, with equivalent terms in 25 additional languages.

Also known as the International Electrotechnical Vocabulary
IEC Customer Service Centre - webstore.iec.ch/csc
(IEV) online.
If you wish to give us your feedback on this publication or need

further assistance, please contact the Customer Service
Centre: [e-mail].
IEC TS 61508-3-2 ®
Edition 1.0 2024-08
TECHNICAL
SPECIFICATION
Functional safety of electrical/electronic/programmable electronic safety-related

systems –
Part 3-2: Requirements and guidance in the use of mathematical and logical

techniques for establishing exact properties of software and its documentation

INTERNATIONAL
ELECTROTECHNICAL
COMMISSION
ICS 25.040.40  ISBN 978-2-8322-9565-6

– 2 – IEC TS 61508-3-2:2024 © IEC 2024
CONTENTS
FOREWORD . 3
INTRODUCTION . 5
1 Scope . 6
2 Normative references . 6
3 Terms, definitions and abbreviations . 6
3.1 Terms and definitions . 6
3.2 Abbreviations . 15
4 Conformance to this document . 15
5 Formal safety requirements specification . 16
6 Formal software architecture / Design specification . 16
7 Higher-level programming languages: Selection of ESCL . 17
8 Compilation to object code . 17
9 Run-time errors and exceptions . 17
10 Applicable techniques . 18
Annex A (normative) Applicable Mathematical and Logical Techniques . 19
Annex B (informative) Specific Mathematical and Logical Techniques . 21
Annex C (informative) Properties assured by application of specific M< techniques . 24
Annex D (informative) Software refinement from safety specification to Code . 26
D.1 Transformation . 26
D.2 Refinement . 26
Bibliography . 27

Table A.1 – M< Techniques . 19
Table B.1 – Specific M< Techniques/Tools . 21
Table C.1 – Properties Assured by M< Techniques . 24

INTERNATIONAL ELECTROTECHNICAL COMMISSION
____________
FUNCTIONAL SAFETY OF ELECTRICAL/ELECTRONIC/PROGRAMMABLE
ELECTRONIC SAFETY-RELATED SYSTEMS –

Part 3-2: Requirements and guidance in the use of mathematical
and logical techniques for establishing exact properties
of software and its documentation

FOREWORD
1) The International Electrotechnical Commission (IEC) is a worldwide organization for standardization comprising
all national electrotechnical committees (IEC National Committees). The object of IEC is to promote international
co-operation on all questions concerning standardization in the electrical and electronic fields. To this end and
in addition to other activities, IEC publishes International Standards, Technical Specifications, Technical Reports,
Publicly Available Specifications (PAS) and Guides (hereafter referred to as “IEC Publication(s)”). Their
preparation is entrusted to technical committees; any IEC National Committee interested in the subject dealt with
may participate in this preparatory work. International, governmental and non-governmental organizations liaising
with the IEC also participate in this preparation. IEC collaborates closely with the International Organization for
Standardization (ISO) in accordance with conditions determined by agreement between the two organizations.
2) The formal decisions or agreements of IEC on technical matters express, as nearly as possible, an international
consensus of opinion on the relevant subjects since each technical committee has representation from all
interested IEC National Committees.
3) IEC Publications have the form of recommendations for international use and are accepted by IEC National
Committees in that sense. While all reasonable efforts are made to ensure that the technical content of IEC
Publications is accurate, IEC cannot be held responsible for the way in which they are used or for any
misinterpretation by any end user.
4) In order to promote international uniformity, IEC National Committees undertake to apply IEC Publications
transparently to the maximum extent possible in their national and regional publications. Any divergence between
any IEC Publication and the corresponding national or regional publication shall be clearly indicated in the latter.
5) IEC itself does not provide any attestation of conformity. Independent certification bodies provide conformity
assessment services and, in some areas, access to IEC marks of conformity. IEC is not responsible for any
services carried out by independent certification bodies.
6) All users should ensure that they have the latest edition of this publication.
7) No liability shall attach to IEC or its directors, employees, servants or agents including individual experts and
members of its technical committees and IEC National Committees for any personal injury, property damage or
other damage of any nature whatsoever, whether direct or indirect, or for costs (including legal fees) and
expenses arising out of the publication, use of, or reliance upon, this IEC Publication or any other IEC
Publications.
8) Attention is drawn to the Normative references cited in this publication. Use of the referenced publications is
indispensable for the correct application of this publication.
9) IEC draws attention to the possibility that the implementation of this document may involve the use of (a)
patent(s). IEC takes no position concerning the evidence, validity or applicability of any claimed patent rights in
respect thereof. As of the date of publication of this document, IEC had not received notice of (a) patent(s), which
may be required to implement this document. However, implementers are cautioned that this may not represent
the latest information, which may be obtained from the patent database available at https://patents.iec.ch. IEC
shall not be held responsible for identifying any or all such patent rights.
IEC TS 61508-3-2 has been prepared by subcommittee 65A: System aspects, of IEC technical
committee 65: Industrial-process measurement, control and automation. It is a Technical
Specification.
– 4 – IEC TS 61508-3-2:2024 © IEC 2024
The text of this Technical Specification is based on the following documents:
Draft Report on voting
65A/1113/DTS 65A/1143/RVDTS
Full information on the voting for its approval can be found in the report on voting indicated in
the above table.
The language used for the development of this Technical Specification is English.
This document was drafted in accordance with ISO/IEC Directives, Part 2, and developed in
accordance with ISO/IEC Directives, Part 1 and ISO/IEC Directives, IEC Supplement, available
at www.iec.ch/members_experts/refdocs. The main document types developed by IEC are
described in greater detail at www.iec.ch/publications.
A list of all parts in the IEC 61508 series, published under the general title Functional safety of
electrical/electronic/programmable electronic safety-related systems, can be found on the IEC
website.
The committee has decided that the contents of this document will remain unchanged until the
stability date indicated on the IEC website under webstore.iec.ch in the data related to the
specific document. At this date, the document will be
• reconfirmed,
• withdrawn, or
• revised.
INTRODUCTION
IEC 61508-1:2010 through IEC 61508-7:2010 forms the series of basic standards for the
functional safety of electric, electronic and programmable electronic systems (E/E/PE systems).
It covers the life cycle of these systems. The major part of the functionality of such systems is
often implemented in software. IEC 61508-3:2010 sets software requirements.
IEC 61508-3:2010 Annex A (normative) and Annexes B and C (informative) contain tables
listing various techniques and measures, and provide some guidance to the selection of such
techniques for different safety integrity levels (SIL). It lists general categories and gives different
levels of recommendation for these, such as "not recommended", "recommended" or "highly
recommended", as well as more specific techniques for various phases of software
development.
These techniques and measures are a mix of generic and specific. The phrase "Formal
Methods" as used in IEC 61508-3 refers to the use of mathematical and logical techniques for
specifying, assessing, designing and verifying software. Today, such methods are available for
specifying requirements, for the assessment of the design, for checking source code and object
code and for the derivation of test suites, and for monitoring the correct operation of software
at runtime. In this document, we refer to these methods by using the description as
mathematical and logical techniques (M< sometimes doubled as M< techniques). Some
of the M< techniques in this document are not restricted to software development, being
equally applicable to other digital-system-based engineering technologies. None of the M<
techniques are limited to the domain of safety-related software systems, although in this
document only safety-related applications of M< techniques are explicitly addressed.
Use of the recommended methods of IEC 61508-3:2010, Annexes A, B and C do not rule out,
for example, susceptibility of the software to run-time failure. State of the art in software
development enables various types of run-time failures to be ruled out through rigorous
development of the software. It is possible using techniques identified here to assure freedom
from many types of software run-time failures.

– 6 – IEC TS 61508-3-2:2024 © IEC 2024
FUNCTIONAL SAFETY OF ELECTRICAL/ELECTRONIC/PROGRAMMABLE
ELECTRONIC SAFETY-RELATED SYSTEMS –

Part 3-2: Requirements and guidance in the use of mathematical
and logical techniques for establishing exact properties
of software and its documentation

1 Scope
This Technical Specification, part of the IEC 61508 series, covers the general assurance of
dependable software used in critical operational-technology (OT) which is running on hardware
devices which are specified as part of the OT application. It is particularly aimed at safety-
related software which is being developed according to the E/E/PE software functional safety
standard IEC 61508-3; in particular, the development of the software follows a Formal Safety
Requirements Specification. Successful use of some or all of the assurance points specified in
this document enhances the confidence that a particular piece of safety-related software meets
the requirements of the SIL of the safety function which it (partially or fully) implements, and
thereby increases the systematic capability of the software.
2 Normative references
The following documents are referred to in the text in such a way that some or all of their content
constitutes requirements of this document. For dated references, only the edition cited applies.
For undated references, the latest edition of the referenced document (including any
amendments) applies.
IEC 61508-3:2010, Functional safety of electrical/electronic/programmable electronic safety-
related systems – Part 3: Software requirements
IEC 61508-4:2010, Functional safety of electrical/electronic/programmable electronic safety-
related systems – Part 4: Definitions and abbreviations
3 Terms, definitions and abbreviations
3.1 Terms and definitions
For the purposes of this document, the following terms and definitions apply.
ISO and IEC maintain terminological databases for use in standardization at the following
addresses:
• IEC Electropedia: available at http://www.electropedia.org/
• ISO Online browsing platform: available at http://www.iso.org/obp
3.1.1
abstract interpretation
static analysis of a program on abstract program states or abstract
machine states that provides sound results for a given property, i.e., that never reports the
property to hold if it does not hold

3.1.2
assurance point
triple, consisting of software and/or documentation
(S1), another SW and/or documentation (S2), and a property P jointly of S1 and S2 such that
P(S1.S2) can be formally mathematically proved
Note 1 to entry: Although a mathematical proof is formally possible at an assurance point, such a proof can be too
complex, or require too many resources, to be given in its entirety and reliably checked, say by an assessor.
3.1.3
automated prover
automated theorem prover
computer program which performs inference in a formal logic between sentences of a formal
language
3.1.4
automated proving
using an automated prover
3.1.5
characteristic function
function (of variable domain) and codomain {0,1} such that its value is
one when its argument belongs to the set or relation, and its value is 0 when its argument does
not belong to the set or relation
3.1.6
code generator
automatic code generator
software which effects the transformation of a high-level language program or a specification
into a common third- or fourth-generation-language program
3.1.7
coding standard
programming-language subsetting
restrictions on the constructs with which a program can be written in a
high-level programming language
Note 1 to entry: The purpose of a coding standard which restricts programming-language constructs that may be
used is to assure an unambiguous semantics to a program written according to the coding standard.
Note 2 to entry: A typical coding standard (n.b., the singular version of this phrase is uncommon) will ensure that
known causes of unreliable behaviour in program code are avoided, e.g., pointer variables are proscribed; undefined
or compiler-variable language features are avoided. Coding standards for programs written in a language without
strong data typing might well ensure that the anticipated or specified range of input or output data is explicitly checked
at input or output.
Note 3 to entry: The term coding standards in general use often refers to further properties of code than subsetting.
3.1.8
compilation
translation operation that translates executable source code level (ESCL) into object code (OC)
Note 1 to entry: The definition explicitly mentions ESCL, a concept used in this document, but not generally where
compilers are used and compilation is practiced.

– 8 – IEC TS 61508-3-2:2024 © IEC 2024
3.1.9
completeness
quality of a formal
language with an associated logic and a formal semantics that holds with respect to a given
semantic property if every sentence of the language having this property can be shown to have
this property through inference in the associated logic
Note 1 to entry: An algorithm is complete with respect to a property if it always proves the property if it holds.
3.1.10
compositional
taking as input just a sentence of a formal language (and not, say, any
indication of context, say the reference of indexicals) and which constructs a transcription purely
using the parse tree of the sentence
3.1.11
computable
recursive
turing-computable
Note 1 to entry: Recursive is used here in the sense in which this term is used in Turing computability and recursive
function theory [1] , [2].
Note 2 to entry: There are in the mathematical literature other notions of “computable” than Turing-computable.
Some are known to be equivalent to Turing-computable, but for some the question is open. This definition thus
disambiguates use of the term “computable”. Similarly, in computer science and system engineering the term
“recursive” has variable meanings; this definition disambiguates use of the term.
Note 3 to entry: The term “decidable” is often used to refer to properties; the term “computable” to functions. A
property is decidable if and only if its characteristic function is computable.
Note 4 to entry: “Turing computable” is a concept which is usually defined over many tens of pages of textbooks on
recursion theory, often using many subsidiary concepts [1] [2]. There lacks a short definition to use here.
Note 5 to entry: There are other notions of computability in logic and computer science which are not, or not known
to be, reducible to Turing-computability.
3.1.12
consistency
property of a collection of sentences of a formal language that they are not contradictory
3.1.13
contradictory
property of a collection of sentences of a formal language when their renderings are mutually
exclusive, that is, they cannot all hold or be realised at the same time in the same structure
3.1.14
decidable
having a Turing-computable characteristic function
___________
Numbers in square brackets refer to the Bibliography.

3.1.15
element
part of a subsystem comprising a single component or any group of components that performs
one or more element safety functions
Note 1 to entry: An element may comprise hardware and/or software.
Note 2 to entry: A typical element is a sensor, programmable controller or final element
[SOURCE: IEC 61508-4:2010, 3.4.5]
3.1.16
element safety function
that part of a safety function which is implemented by an element
[SOURCE: IEC 61508-4:2010, 3.5.3]
3.1.17
executable source code level
ESCL
source code at which the exact behaviour of the software is completely described
3.1.18
formal inference
derivation of a sentence from premises using the explicit formal rules of inference
of the logic
3.1.19
formal language
language with a defined syntax which is parsable without exception by means of
digital computation, and such that it is computable whether a given sequence of symbols forms
a sentence of the language or not
Note 1 to entry: The term “sentence” is used in this document for a member of a formal language, but in many
formal languages other terms are more appropriately used. When a formal language consists of strings of symbols
simpliciter, as do formal languages in formal language theory, automata theory, and formal logic, then a well-formed
member is called a sentence, except in formal logic, where it is called a well-formed formula. In programming
languages, a well-formed member is called a valid program, and in specification languages, a well-formed member
is called a valid specification. In diagrammatic languages, a well-formed member would be called a valid diagram.
Note 2 to entry: This notion of formal language is that used in logic, linguistics, mathematics, formal language
theory, automata theory and theory of compilation. Formal languages such as (engineering and software)
specification languages also often come with a preferred formal semantics (e.g., Z, TLA) and the use of the term in
such software engineering contexts often implicitly includes the formal semantics.
Note 3 to entry: In mathematics and automata theory, the term formal language denotes just a set of strings of
symbols from a defined symbol set, with no constraints upon how these strings are formed. However, all the formal
languages used in M< satisfy the conditions given in the definition.
Note 4 to entry: In formal logic, the term “language” (without the prefix “formal”) customarily refers to the set of non-
logical symbols. The set of logical symbols of a formal language of logic is customarily taken to be determined,
although it varies between first-order logic and higher-order logics.
3.1.20
formal logic
propositional logic, predicate logic, higher-order logic, combinatory logic, modal logic, non-
classical logic, other mathematical language structure based on a formal language which has
a notion of formal inference, consistency and contradiction
3.1.21
formal proof
written formal inference of the
sentence in the formal logic, using as premises the sentences in the given set

– 10 – IEC TS 61508-3-2:2024 © IEC 2024
3.1.22
formal semantics
< of a language> precise mathematical rendering of the (intended) meaning of the sentences
of a formal language, such that any two sentences identical in meaning have the same
rendering, and any two sentences which differ in meaning have different renderings
Note 1 to entry: A formal semantics has some or all of the structure of a semantics of a formal logic.
Note 2 to entry: In most formal semantics, two sentences with identical meaning can initially receive differing
transcriptions, and it can be the case that these transcriptions have to be further manipulated, say by using a formal
“reduction agent”, such as a theorem prover or checker, to render the judgement that the renderings, namely the
transcriptions reduced by the reduction agent, are identical. The rendering in this case consists in transcription,
followed by reduction when it is necessary to determine if two sentences have identical meaning or not.
Note 3 to entry: There is no requirement that it be computable whether two sentences have the same meaning.
Identity of meaning can be semi-computable, but it must be at least semi-computable.
3.1.23
formal semantics
rendering of the sentence in the formal (language) semantics
3.1.24
formal specification
functional specification written in a formal language with a formal semantics
3.1.25
formal verification
mathematically rigorous argument or method to guarantee that required properties
are satisfied
Note 1 to entry: Some formal verification methods work to a specified level of confidence less than certainty.
Note 2 to entry: Examples of formal verification methods are theorem proving, model checking, and abstract
interpretation.
3.1.26
fulfil
specification> be such that the rendering of the (object) specification can be formally proven
from the rendering of the software object/(subject) specification in a formal logic
Note 1 to entry: The terms “(subject) specification” and “(object) specification” are used here to indicate which of
two specifications is the subject, respectively the object, of the verb “fulfil”.
3.1.27
intermediate executable specification
IES
source code at a programming-language level chosen to be above that of the executable source
code level, when multiple levels of source code exist, according to 6.1

3.1.28
level
sublanguage of a high-level programming language which is
related by syntactic transformation to other levels – other sublanguages – of the programming
language
EXAMPLE 1 The programming language Java has so-called “source code” and bytecode. Java bytecode is
generated by a Java compiler from Java source code. Java source code is a level; Java bytecode is a level. The
Java source code level is “above” the Java bytecode level.
EXAMPLE 2 Commonly-used programming languages, for example C and C++, have “standard libraries”, which
consist of more or less complex functions which are invoked in source code using a single identifier. C source code
which uses the identifiers for library functions is a level, say C.1. Assume further that C.1 is a subset of C which only
uses terms and operators with explicit, unambiguous semantics. C.1 code in which the library functions have been
replaced by in-line code which does not involve the library-function identifiers, or only involves some but not all of
them, also forms a level, say C.2. C1 is “above” C.2 because source code in C.1 is transformed into source code in
C.2 with the same meaning through replacing the library functions not in C.2 with in-line code executing those
functions.
Note 1 to entry: A programming language level L.1 is said to be “above” another level L.2 if both L.1 and L.2 are
rigorously syntactically defined and a program in L.1 is transformable using common programming-language
technology into a program in L.2 with the same semantics.
3.1.29
model checker
software which performs model checking on program code
3.1.30
model checking
enumeration of
a collection of states and checking for each state in the collection whether a given state property
is fulfilled or not
Note 1 to entry: Model checking is often performed using abstract states for reasons of practicality due to the
combinatorics involved. The power of model checking lies largely in the method of abstraction, which attempts to
cover a lot of actual program states with as few abstract states as possible in order to check the property effectively.
3.1.31
object code
executable code installed directly on, and executable directly on, digital-computational
hardware
3.1.32
proof checker
automated proof checker
software which takes machine-readable formal proofs in a formal logical language and returns
a value indicating whether the proof is a correct proof or not
3.1.33
refinement
act of transforming an intermediate executable specification into another intermediate
executable specification or executable source code level preserving the formal semantics of the
original specification but with more detail about execution
EXAMPLE 1 The transformation of Java source code into Java bytecode is refinement.
EXAMPLE 2 The transformation of C.1 into C.2 in EXAMPLE 2 of 3.1.28 is refinement.
EXAMPLE 3 The transformation of a state-machine description into, say, C code implementing that state machine
is refinement.
– 12 – IEC TS 61508-3-2:2024 © IEC 2024
3.1.34
relative completeness
completeness in which the semantics of sentences are partially given
by outside constraints
Note 1 to entry: Formal semantics are compositional when they allow deduction of (semantics) transcriptions purely
from sentences (see 3.1.17) without using context, purely using the parse tree of the sentence. Some useful formal
semantics are non-compositional; context must be used to determine the meaning of a statement. Using context in
this way is an example of a semantics being partially given by outside constraints.
3.1.35
rendering
< of a sentence in a formal semantics> form by means of which a sentence is determined to be
identical in meaning to or different in meaning from another sentence
3.1.36
rigorous
unambiguous and explicitly understood to cover all possible behaviours
and capable of being thoroughly checked for aspects of correctness and incorrectness
3.1.37
rigorous
conducted using formal inference and capable of being thoroughly
checked for aspects of correctness and incorrectness
3.1.38
rigorous
carried out with attention paid to each and every process step to ensure that it
has been correctly executed
3.1.39
runtime verification
technique whereby monitoring variables are placed in program code, whose values represent a
partial program state which indicates in greater or in less detail whether a computation is
correctly running, and raises an alarm or an exception when this is not the case
3.1.40
safety function
function to be implemented by an E/E/PE safety-related system or other risk reduction
measures, that is intended to achieve or maintain a safe state for the EUC, in respect of a
specific hazardous event
EXAMPLE Examples of safety functions include:
– functions that are required to be carried out as positive actions to avoid hazardous situations (for example
switching off a motor); and
– functions that prevent actions being taken (for example preventing a motor starting).
[SOURCE: IEC 61508-4:2010, 3.5.1]
3.1.41
schedulability analysis
analysis determining if all tasks can be scheduled by a given scheduling algorithm to run and
finish before their deadlines
3.1.42
semi-computable
semi-decidable
recursively enumerable in the sense in which this term is used in Turing computability and
recursive function theory
Note 1 to entry: See [1], [2].
3.1.43
sentence
string of symbols which is a well-formed member of the language
Note 1 to entry: When a language is taken to be simply a set of strings of symbols, then a sentence of the language
is simply a member of this set
Note 2 to entry: When the formal language is a formal specification language, a sentence in this sense is often
called an assertion, or a condition, or a module (of those specification languages which require modules). When the
formal language is the language of a logic, a sentence in this sense is called a well-formed formula. When the formal
language is a programming language, a sentence in this sense is a (valid) program, which is not conventional in
programming-language theory.
Note 3 to entry: In computer science, there are diagrammatic languages, such as those for some forms of automata,
or for defining hierarchies of classes of data, or for illustrating interprocess communication, that can also be
considered a form of formal language, even though they do not consist of strings of symbols, but rather of certain
spatial arrangements of symbols, often two-dimensional. It seems inappropriate to call these sentences. The
definition of “well formed” equally applies to such arrangement-languages.
3.1.44
sound
exhibits the property of soundness
3.1.45
soundness
quality of the logic and formal semantics that
holds if, whenever the logic proves a sentence of the language, this sentence is logically valid
in the formal semantics
3.1.46
soundness
quality of a static analyzer and
a formal semantics that holds if, whenever the analyzer makes an assertion S, S is logically
valid with respect to the formal semantics
Note 1 to entry: If assumptions A1, A2, …, An are used by the analyzer to assert S, then S is to be valid under
these same assumptions; i.e., the sentence (A1 ∧ A2 ∧…∧ An → S) is logically valid with respect to the formal
semantics.
Note 2 to entry: This definition applies to any static formal verification tool, including theorem provers and model
checkers.
Note 3 to entry: It can often be the case that the formal semantics being used is undecidable, hence that there is
no algorithm for exceptionlessly checking that S is logically valid with respect to the semantics. When practical
checking fails, this is most often for reasons of complexity that do not relate to the undecidability of the underlying
semantics; undecidability is mostly not a practical hindrance to such checks.
3.1.47
source code
program written in a formal higher-level programming language
3.1.48
static analysis
analysis of the properties of a program or a specification in a formal language through analysis
of the text of the program or the specification rather than through execution or partial execution

– 14 – IEC TS 61508-3-2:2024 © IEC 2024
3.1.49
systematic capability
measure (expressed on a scale of SC 1 to SC 4) of the confidence that the systematic safety
integrity of an element meets the requirements of the specified SIL, in respect of the specified
element safety function, when the element is applied in accordance with the instructions
specified in the system manual for compliant items
[SOURCE: IEC 61508-4:2010, 3.5.9]
3.1.50
theorem prover
software whose primary input consists of putative theorems and a set of premises in a formal
logic and which attempts to determine if there is a formal proof of the putative theorems in the
logic or not
Note 1 to entry: A theorem prover is for a specific (and specified) formal logic.
Note 2 to entry: A theorem prover can succeed on given input (it identifies a proof), or fail (it has not identified a
proof). Failure does not necessarily mean that there is not a proof in the logic. A theorem prover for which failure
entails that there is no proof in the logic is known as a "decision procedure".
Note 3 to entry: Some logics preclude that any computational engine can always deliver a correct yes/no answer in
every case, so theorem provers are often based on algorithms which are necessarily incomplete.
Note 4 to entry: There are many forms of theorem provers, ranging from "proof checkers", which are not interactive
and concomitantly require possibly considerable logical work in advance from the human user, to "proof assistants"
or "interactive theorem provers" which exhibit various levels of interaction with a user, who "guides" a proof towards
the desired goal.
3.1.51
transcription
written form into which the sentence
is translated in a formal semantics, before any reduction is applied to determine the rendering
3.1.52
unambiguous
having a unique rendering in a formal semantics up to logical
or behavioural equivalence
Note 1 to entry: This definition does not formally fulfil the substitutability criterion for terms: “X is unambiguous”
would be rendered as “X is has a unique….”. However, readers can resolve the phrase “is has” easily.
3.1.53
undecidability
category of decision problem complexity implying that there is no automatic algorithm that
always proves the decision true if it holds (completeness) and never proves the decision true if
it does not hold (soundness)
3.1.54
undecidable
not decidable
Note 1 to entry: If a form of formal reasoning is undecidable, it follows that there is a formal logic which
accomplishes this reasoning (or is generally understood to do so) and that there is no algorithm for determining
whether a given well-formed formula of the logic is provable or not provable. However, while it can be important to
know that the problem being addressed is undecidable, the practical issues involved in using theorem provers on
concrete problem instances usually vastly outweigh any issues that can arise through the undecidability of the
underlying logic. For many undecidable problems sound algorithms provide practical solutions.

3.1.55
well-formed
valid member of the formal language built up according to the rules of
definition of the language
Note 1 to entry: If the formal language consists of simple strings of symbols, as in a regular language or context-
free language, such as the language of a formal logic, then a well-formed member of the language is often called a
sentence. If the formal language is a programming language, a well-formed member is called a valid program. If the
formal language is a formal specification language, a well-formed member is called a specification.
Note 2 to entry: In computer science, there are diagrammatic languages, such as those for some forms of automata,
or for defining hierarchies of classes of data, or for illustrating interprocess communication, that can also be
considered a form of formal language, even though they do not consist of strings of symbols. Such arrangements
constructed according to the formation rules of such a diagrammatic language are well-formed according to this
definition.
3.1.56
worst-case execution time analysis
WCET analysis
analysis resulting in a trustworthy upper bound on the length of time it takes the machine
instructions of a specific task to run on specific hardware
Note 1 to entry: WCET analysis assumes non-interrupted execution of a task. Effects of task preemption and
blocking are considered during schedulability analysis.
Note 2 to entry: Interference effects that can affect the non-interrupted execution time of a task, e.g., due to
conflicting accesses to resources shared between different cores of multi-core systems, are counted to the WCET.
The non-interrupted worst-case execution time of a task discounting such interferences is typically called intrinsic
WCET.
3.1.57
worst-case response time analysis
WCRT analysis
analysis resulting in a trustworthy upper bound on the maximal time it takes a task invocation
to complete all its activity relative to its arrival time
Note 1 to entry: The arrival time is the time at which a task invocation is ready to start running.
Note 2 to entry: Aspects of the worst-case response time of a task include its worst-case execution time, the time
it is preempted by higher-priority tasks, and the time it is blocked on synchronization primitives
3.2 Abbreviations
ESCL Executable Source Code Level
FSRS Formal Safety Requirements Specification
IES Intermediate Executable Specification
M< Mathematical and logical techniques in systems engineering
OC Object Code
SWA/DS Software Architecture/Design Specification
WCET Worst-Case Execution Time
4 Conformance to this document
To conform to this technical specification, it shall be demonstrated that all the relevant
requirements have been satisfied to any required criteria specified and therefore, for each
clause, all the objectives have been met. The demonstration shall include justification of the
selection of requirements as relevant, based on the claimed application of M< techniques
across the software lifecycle.
NOTE Conformance to this technical specification does not require satisfaction of every clause, only those relevant
to the lifecycle aspects to which mathematical and logical techniques are applied.

– 16 – IEC TS 61508-3-2:2024 © IEC 2024
5 Formal safety requirements specification
5.1 An unambiguous, rigorous formal safety requirements specification (FSRS) shall be
written for software components.
NOTE 1 The FSRS required in 5.1 is suitable to fulfil the requirement of IEC 61508-3:2010, 7.2, that is, the FSRS
is a software safety requirements specification as required by IEC 61508-3:2010, 7.2.
NOTE 2 According to IEC 61508-3:2010 7.4.2.8, when the software implements some safety function, then the
entire software is safety-related and the associated software requirements specification includes a safety
requirements specification.
NOTE 3 There are three main ways in which a safety requirements specification could ultimately be inadequate.
First, it could fail to govern some safety-related behaviour which it should indeed subsume (that is, fail to exclude
some evidently dangerous system behaviour). Second, it could be ambiguous, and through the ambiguity allow some
dangerous behaviour which could be excluded in an unambiguous specification. Third, it could use a formal
specification language which is inadequate to capture some distinctions between non-dangerous and dangerous
behaviours, and thereby exclude some non-dangerous behaviours which are in fact benign, unnecessarily restricting
the system developed. The adequacy of a software safety requirements specification is governed by IEC 61508-
1:2010, 7.10 and IEC 61508-3:2010, 7.2 and is not completely determined by Clause 4 of this document.
NOTE 4 A language for the FSRS is not specified he
...