This page is in group Technology. Also see Standard disclaimer
Scratchpad 1
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 [1] is IEC 61508 approved. 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? Update 22May2019: Express Logic has been acquired by Microsoft (here). They claim that «Express Logic’s ThreadX RTOS has over 6.2 billion deployments, making it one of the most deployed RTOS in the world per VDC Research.» They continue with «Over 9 billion of these MCU-powered devices are built and deployed globally every year, many of which can benefit from Express Logic solutions». This is so large a number that it’s hard to grasp! Update 03Nov2023: Plus it’s supposed to be 10 billion deployments, per VDC Research 2020! Another point, search for PX5 RTOS (below)
- The Wind River® VxWorks® Cert Platform [2] 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 [3]. 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 certified. See [5]. 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 [4] 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?
- Update Nov2020: XMOS introduces a new development system with FreeRTOS and TensorFlowLight conversion, for machine learning [9]. Perhaps not for IEC 61508, but then, maybe..?
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?
Scratchpad 2
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 [6]. 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 [7]. 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.»)
- At the IEEE-COPA 2021 (via here) the seL4 was mentioned, during the discussions. It is able to do worst-case execution-time (WCET) calculations
- PharOS (Asterios® at Krono Safe). At Leslie Lamport’s discussion page about his TLA+ videos I found a reference to PharOS [8]. «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
Scratchpad 3
- New 02Nov2023. I learn that the PX5 RTOS [10] has the same author origin as ThreadX. See Bill Lamie at LinkedIn, here. PX5 RTOS has support for the Arm® TrustZone®, a system where (for 32 bit Arms, at least it looks like this from the Wikipedia page ARM architecture family) virtual processors are set up, and thus duplication to some point. PX5 RTOS also has a patent-pending Pointer/Data Verification (PDV) technology, which is a lightweight encapsulation of objects with tiny hashes for certain important data. This will detect memory corruption issues, allowing the system to try to mitigate this, by f.ex. doing a soft reset, provided the system as such would allow this. (Aside: To reset a plane shows that this is not at all obvious.) PX5 RTOS also has a low memory footprint, even if (or perhaps since) it is based on a native implementation of the industry-standard POSIX pthreads API. Systems built with PX5 may be deterministic as well. I couldn’t tell exactly what this implies. According to their web page (login and search) they plan to have PX5 RTOS IEC 61508 certified «later this year».
- Update 08Nov2023. From a brag email abot the announcement of PX5 NET. I add this here because I like it, but I haven’t tested it myself. (Observe my Standard disclaimer.) Now pthreads+ seems to have appeared in the text. It’s not on Wikipedia, is this a term PX5 have coined themselves?
«Like all PX5 products, PX5 NET is based on the industry standard BSD Sockets API to significantly reduce developers’ learning costs, increase productivity, and maximize the reuse of existing programs and libraries. Widely implemented across the embedded industry – including embedded Linux – the combination of the BSD Sockets API and PX5 RTOS’ native POSIX pthreads+ API eliminates the need for any “adaptation layers” and reduces compatibility issues that frequently plague development teams. Additionally, PX5 NET provides clearly identified API extensions for zero-copy transmission and reception, packet management, and functionality on top of BSD Sockets that allows developers to fine-tune system behaviors. .. including semaphore, mutex, and message queues, and offers real-time extensions such as event flags, fast queues, tick timers, and memory management.«
References
[1] http://en.wikipedia.org/wiki/Threadx, is there a user group?
[2] http://en.wikipedia.org/wiki/Vxworks, user group at comp.os.vxworks
[3] http://en.wikipedia.org/wiki/TIPC, Transparent Inter-Process Communication. Cert: http://www.windriver.com/products/platforms/vxworks_cert/
[4] http://en.wikipedia.org/wiki/QNX#Technology
[5] http://www.electronicsweekly.com/news/intel-certifies-xeon-processor-safety-critical-design-wind-river-2016-12/
[6] 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
[7] 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
[8] 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
[9] XMOS announces all-new software development kit for the artificial intelligence of things, Oct2020, see https://www.xmos.ai/xmos-announces-all-new-software-development-kit-for-the-artificial-intelligence-of-things/.
[10] THE INDUSTRIAL GRADE PX5 RTOS, see https://px5rtos.com/px5-rtos/