[SystemSafety] IEC Technical Specification on Formal Methods

[Peter Bernard Ladkin]

Folks,

I have been working since 2010 in the German National Committee for a clearer specification of the
use of formal methods in dependable software development according to IEC 61508. Currently, IEC
61508:2010 "highly recommends" the use of "formal methods" for software implementing safety
functions with a SIL 3 or SIL 4 requirement. That is about it. It doesn't say what is meant by
"formal methods" or give any guidance as to how and where they can be used, or for what.

IEC project proposal 65A/867/NP was circulated amongst participating members of IEC SC 65A (32
countries) earlier this year.  The proposal identifies over 20 properties of SW and its
documentation which may be assured using industrially-mature formal methods (and in most cases not
assured unless formal techniques are used).

I gave a Keynote talk on this topic at the 6th Scandinavian Conference on System and Software Safety
in Stockholm on May 21. The annotated slides from the talk may be found at
http://safety.addalot.se/upload/2018/SCSSS18_BernardLadkin.pdf

The list of SC65A members, along with participation status, and how they voted, may be found at
http://www.iec.ch/dyn/www/f?p=103:52:0::::FSP_ORG_ID,FSP_DOC_ID,FSP_DOC_PIECE_ID:1369,1010654,318821
20 participating members voted yes; a simple majority of 17 is needed. However, only four countries,
namely China, France, Germany and the UK, nominated experts (this is the IEC term for people
nominated by their National Committees who participate in IEC standards-committee meetings). At
least five countries need to nominate experts for the proposal to go ahead. But we only have four.

We have about two weeks to find another participating country who will nominate an expert. The list
of countries who could do so and have not yet done so is Australia, Austria, Canada, Finland, India,
Ireland, Italy, Japan, Korea, Malaysia, Pakistan, Poland, Romania, Russia, Slovakia, Sweden,
Thailand. If anyone here is involved in engineering standardisation in any of these countries, and
thinks that more precise guidance on the use of formal methods in safety-critical software is
necessary, I would encourage you to get in contact with your National Committee to propose a
working-group participant. The SC 65A secretary, Petar Luzajic at BSI, only needs an email stating
such an intention from a National Committee of one of these countries for the project formally to go
ahead.

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
MoreInCommon
Je suis Charlie
Tel+msg +49 (0)521 880 7319  www.rvs-bi.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20180621/fc74bc28/attachment-0001.sig>