I plan to scribble on this note to discuss some, in my opinion, peculiar aspects of the IEC 61508 functional safety-critical standard.
I will only discuss process safe (or thread safe) programming in IEC 61508 context. Is the IEC 61508 end user safe in this respect?
Here are some points (I will watch out for more):
- ThreadX by Express Logic  is IEC 61508 approved. The wikipedia-page doesn’t state this, but Express Logic’s own pages do. It sends pointers to shared data over its message queue if the message is longer than, say, 16 bytes. How is usage of this reasoned for the 61508 approval agencies?
- The Wind River® VxWorks® Cert Platform  is IEC 61508 approved. The wikipedia-page doesn’t state this, but Wind River’s own pages do. I have asked some questions about the semantics of their message channels at comp.os.vxworks, read here. Their documents made me uncertain. However, their message channels are built on TIPC . Their TIPC also supports shared memory. They also have “cache, clock, event flag, interrupt, memory management, message queue, ring buffer, semaphore, signal, and task management calls, along with a wide array of C library functions.” And “User mode applications are supported with real-time processes (RTP) to a safety-certifiable environment.”
WindRiver has a DVD where I think that configuring the different components related to their degree of approval is described. It looks to me like it’s the network stack and file system that are really certified. “This certification package DVD contains the VxWorks Cert Platform Safety Manual and all required IEC 61508 SIL 3 documentation.”
- Update Jan2017: WindRiver has got the Intel® Xeon® processor D-1529 industrial processor IEC 61508 certificatied. See . This is probably mostly for large robots.
- When is proven in use too little to write home about and proven for use too difficult to do?
- I have a blog note here, “Some questions about SDL” (056) where I implicitly try to argue that CSP would be better suited for 61508 than SDL. But I doubt my level of success, seen in most other sw engineers’ eyes?
- I am more inclined to like the QNX  communication model, with my CSP channel type communication experience. I would argue that this model is more IEC 61508 “friendly”?
- I branch off this blog note to particularly handle “IEC 61508 and concurrency“
- SafeRTOS (IEC 61508 compliant by Real Time Engineers Ltd. and WITTENSTEIN HighIntegritySystems ), see note 122. (FreeRTOS and OpenRTOS are cousins)
- Update Jan2017: Intel has a “IEC 61508 SAFETY RUNTIME SYSTEM” caleld SAFEOS. Search for it in note 122 (previous line)
I will come back to this whenever I see or suspect rather unsafe programming techniques, that the manufacturers still show to be IEC 61508 compliant.
Disclaimer: a potentially unsafe programming technique is not a “formal” rejection criterion, if that coding may be shown to have been done correctly. IEC 61508 is preoccupied with safety, and if it’s correct, it’s safe. But is this at the same time contrary to the 61508 standards documents, which list a huge number of good practices?
Formally proven kernels
This is just a list for myself (and perhaps you) of RTOS or kernels that are claimed to have been formally verified fram A to Z. This is very interesting. Standard disclaimer, of course.
- Formal Development of a Network-Centric RTOS by Eric Verhulst et al. See . It’s also available for XMOS., according to their web page. I am very curious about that (TODO). It’s by company Altreonic. Since 2016(?) this system is the basis of the KURT electric car platform
- seL4: Formal Verification of an OS Kernel by Gerwin Klein et al. See 
- http://en.wikipedia.org/wiki/Threadx, is there a user group?
- http://en.wikipedia.org/wiki/Vxworks, user group at comp.os.vxworks
- http://en.wikipedia.org/wiki/TIPC, Transparent Inter-Process Communication. Cert: http://www.windriver.com/products/platforms/vxworks_cert/
- Formal Development of a Network-Centric RTOS by Eric Verhulst, Boute, R.T., Faria, J.M.S., Sputh, B.H.C., Mezhuyev, V. In series Software Engineering for Reliable Embedded Systems. See http://www.springer.com/us/book/9781441997357
- seL4: Formal Verification of an OS Kernel by Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. In Proceedings of the ACM SIGOPS 22nd symposium on Operating system principles. SOSP ’09, 2009. See http://dl.acm.org/citation.cfm?id=1629596