Abstract. OpenComRTOS is one of the few Real-Time Operating Systems (RTOS) for embedded systems that was developed using formal modeling techniques. The goal was to obtain a proven trustworthy component with a clean and high performance architecture useable on a wide range of networked embedded systems. The result is a scalable communication system with real-time capabilities. Besides a rigorous formal verification of the kernel algorithms, the resulting architecture has several properties that enhance the safety and real-time properties of the RTOS. The code size in particular is very small and typically 10 times less than a typical equivalent single processor RTOS. 1 Problem Statement Following a market research study for the European Space Agency in 2004, it was discovered that the majority of the RTOS (Real-Time Operating Systems) on the commercial as well as on open source market, cannot be verified or even certified, e.g. according to the DoD 178B or IEC61508 standards. This i...
Eric Verhulst, Gjalt G. de Jong