The book on the OpenComRTOS project is out. Lessons learned.

The book is now available from Springer and Amazon.

While published by a scientific publisher, this book is not a purely scientific one. But it shows how the state of the art in science can be applied to a real industrial development with great benefit. It documents (incompletely but sufficiently) the journey of the OpenComRTOS project. This project started out with the goal to see how we could apply formal methods to embedded software development. And because we had a background in a distributed Real-Time Operating System, we decided to use the design from scratch as a target. Not a trivial one as it covers concurrency, protocols, local as well distributed state machines as well as boundary conditions of efficiency, hard real-time capability, scalability and other non-functional requirements. An RTOS is however a suitable and grateful target as it is the key layer between hardware and application software.

Therefore, the book starts by situating the project in a larger context of trustworthy systems engineering, ventures into selecting a formal technique, describes some of the abstract design models, ventures even deeper into the formalism used but ends gracefully with a discussion on the interaction semantics, performance obtained and how to visually program with it. It is only about a few KBytes of code, but in the end it requires venturing into many different and diverse aspects.

The most important however is what did we learn during the project?

1. Formal methods are not necessarily that hard to apply.

Granted, one needs people with a decent mathematical schooling but nothing spectacular. Granted also, the initial learning curve, partly related to the notation, is steep. But given that this was the first use of Formal Methods, it was not worse than learning another programming language. 

2. Formal methods really shine when used as a design tool.

Often Formal Methods are put forward as software verification tools only. While this is very useful, the verification is the often at the level of the final source code in the particular programming language used. Often, this will expose weaknesses of the language used but not the weaknesses in the language independent architecture. The benefits from using formal methods as a design tool is that they provide a level of abstraction that helps a lot to think anew about the system to be developed and without immediately starting to think in terms of an implementation.

3. Architecture matters. Code size still matters.

One of the unexpected (quantitative) results of the use of formal methods was that the software architecture matters most. Actually, a clean architecture is the result of an abstract analysis combined with some well thought out choices, the latter often inspired by experience. The result is not only a "correct by design" RTOS, but also a much more efficient. In this case, the code size was about 5 to 10 times smaller than a handcrafted equivalent RTOS. Other benefits are scalability, portability, safety, security, etc. In combination with code generators, the developer is freed from writing error-prone initialization code.

4. Formalization is more important than going formal.

While formalization is a pre-condition for applying formal methods, in itself it provides many benefits without having to dig into the details. It helps a lot to understand the problem domain and a problem well understood leads to cleaner and simpler solutions. The main benefit is orthogonalisation. Orthogonalisation is the key to a clean architecture and the key to avoid unplanned side-effects. As a result, OpenComRTOS has exceptionally clean but surprisingly straightforward and predictable semantics.

Looking for clean semantics was also a great help in defining OpenComRTOS meta-models. These are very helpful for example in maintaining portability and defining platform level support.

5. Formalization pays off.

Another benefit is that while formal developments have a steeper starting slope, this is paid back twice or more in the long term. The small code and build-in transparent communication translates directly in the capability to use slower processor with less memory. Hence, it helps to reduce power consumption. It also helps in engineering costs. For example, porting the RTOS to a new processor is now done in one or two weeks vs. often months to a year for the previous hand coded version. It also pays off for security (OpenComRTOS cannot have buffer overflows), for scalability (because the underlying architecture uses packet switching), for ease of use (the visual modeling environment will generate a heterogeneous distributed application in minutes), etc.

6. The devil is in the details.

Where formal verification really helps is in the details. While a simple RTOS has nothing more than a tasks scheduler and a synchronization/communication primitive, the complexity can rise fast when real-world functionality is added. Priorities, preemption, waiting lists, time-outs, resource locking, priority inheritance, etc. often require conflicting implementations. To get it right, the semantics must be carefully designed while the implementation must be kept to a minimum. Formal verification helps in finding loose corner cases while the orthogonality of the core architecture contributes to an efficient implementation.

7. Concurrent programming works.

One of the very original project requirements was to have a solution for the idea of "program it once, run anywhere", with this important detail that anywhere was defined as any number and any type of processors, being connected anyway it is. OpenComRTOS can do it. The key is the clean concurrent programming model (inspired by Hoare's CSP process algebra) and clean interaction semantics. The latter is delivered by the "hub" concept, an OpenComRTOS specific mechanism that implements very efficiently events, semaphores, fifo's, resources, ports, memory pools, etc. What's more, it inherits the elegance of a fundamental construct of the formal methods world: a hub is like a guarded atomic action and that's what gives it's scalability and efficiency. The programming model of OpenComRTOS is also not limited to programming with ANSI-C. A recent prototype was developed that implements the functionality in Python. This can be extended to any programming language bringing the concept of universal programming to a new level.

8. We can learn from telecom

A key, but logical choice, was to make intensive use packet switching at all levels, even if that is not really visible at the application level. It avoids copying parameters, it helps to protect the integrity of the system and it reduces the overhead, especially when remote nodes and hubs are involved. Packets also eliminate buffer overflows and make fault tolerance a lot easier to implement. What telecom systems do in the large, OpenComRTOS does at the small scale of embedded devices. 

9. The roadmap after the project.

Now that the ground layer is finished (that includes a lot of visual development tools), we can think about next steps (of which some are already in the works), such as:

• Fault tolerance: while easy to program by hand, why not turn this into a compile time option? The architecture and code generators make it possible without changing the original application source code (assuming to be well written).
• Protocol composition: similarly, code generation from higher level specifications can generate application protocols as reusable blocks.
• Distributed priority inheritance: this was already implemented and was released in v.1.4.
• Asynchronous services: while already in place with single processor support, asynchronous versions of the task interaction services are a tough challenge for the semantics and the resource constraints of the embedded world.
• General resource scheduling: embedded systems are becoming less static and hence priority based scheduling of CPU time is no longer sufficient to guarantee a predictable Quality of Service. We have the concepts in place to extend the scheduling to all kinds of resources, even if the available resources might not be sufficient to satisfy all demands simultaneously.
• Dynamic code: This is a very tough requirement in distributed heterogeneous and resource constrained embedded systems. Using a formalized approach, we developed a solution that allows us to execute any binary code as a normal real-time task on any C programmable processor requiring just a few KBytes. In combination with distributed component based services, this is a powerful mechanism for diagnostics, encapsulating legacy code, fault tolerance and many more applications.

After the book, comes the try-out.

In line with the project requirements of "program once, run it anywhere", one of the first versions to be developed was a version running on top of MS-Windows. As such a PC (or any node running a host-OS like Linux or any other RTOS), can be used to simulate a networked application or transparently integrated as a node in a larger network. Once developed, remapping to an attached or different processor or networked system of processing nodes is mainly a matter of recompilation of the source code. You can try it out and get a feeling for how easy concurrent/parallel programming can be. No need for a special multicore, manycore or parallel processing library. Download it from the Altreonic website. (contact us if you have issues).