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)
- Update 27Mar2017: Asterios by Krono-Safe, see below. In the certification process for IEC 61508. However, “the first certified versions of ASTERIOS are due in 2015 and 2016” indicates that they still are in that process?
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 done in Leslie Lamport’s TLA+. It’s by company Altreonic. Since 2016(?) this system is the basis of the KURT electric car platform. (See Zephyr operating system (here) to read a side-text on this)
- seL4: Formal Verification of an OS Kernel by Gerwin Klein et al. See . This is a “high assurance L4“, covered in Wikipedia here (“The proof provides a guarantee that the kernel’s implementation is correct against its specification, and implies that it is free of implementation bugs such as deadlocks, livelocks, buffer overflows, arithmetic exceptions or use of uninitialised variables.”)
- PharOS (Asterios® at Krono Safe). At Leslie Lamport’s discussion page about his TLA+ videos I found a reference to PharOS . “Executions in the PharOS real-time system are deterministic in the sense that the sequence of local states for every process is independent of the order in which processes are scheduled” and “Fortunately, it is possible to design concurrent real-time systems such that their behavior does not depend on the order of scheduling, as long as all components have access to a common time base”. “Avoiding race conditions between processes is crucial for achieving the first objective.” “Agents communicate with one another exclusively by asynchronous message passing”.
(I started a thread on this at Xcore, here)
- XMOS guaranteed determinism. The whole processor architecture is built so that the tools may analyse #pragma-driven “unique timing deterministic architecture”. Start at XMOS. I have discussed this in note 049. I haven’t seen any formal proofs of this, so it’s formally off the point here. But still
- … probably lots. Probably enough to preempt this list
- 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
- Proving Determinacy of the PharOS Real-Time Operating System by Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, and Stephan Merz © Springer 2016 at https://members.loria.fr/SMerz/papers/abz2016-pharos.html