You are here Altreonic at FM2009 and CPA2009
Altreonic at FM2009 and CPA2009
This year the formal community met in Eindhoven (see FM week) . It was a unique opportunity as it brought together specialists from all over the world. It was also one of the first times that several complementary groups held their conference at the same location and in the same week. Altreonic had a well received paper at CPA ("OpenComRTOS: A Runtime Environment for Interacting Entities", see attached pdf). Formal methods are becoming not only mainstream but also a prerequisite in any development that has safety or security requirements. This is now clearly reflected in the recent versions of the IEC61508 and DO-178 safety standards. An interesting keynote was given by Jeannette Wing, professor at Carnegie Mellow and Assistant Director at the US National Science Foundation. While the topic was "Formal Methods for Privacy", she addressed the definition of what is meant with trustworthy systems very well. Simply said: Trustworthy = safety + security + privacy + usability.
In addition, she made it clear that privacy has deep roots. To really understand it (and that's a precondition for implementation in software) one needs to go back to its origin in fundamental rights like liberty, freedom of expression and property rights, the same fundamental concepts that justify the need for safety and security. Trustworthy systems are also at the heart of Altreonic's objectives. One thing that was noticed is that there is still a long way to go to integrate the early requirements and specifications capturing (prior to modeling) in the engineering process. As such, Altreonic is pioneering this integrated view.
In this integrated view, formal methods are supporting tools in the formalisation. In an early stage, they support the design process by raising the abstraction level away from existing implementation patterns. Architectures become cleaner because the formal approach unveils where there is overlapping functionality and where extra implementation levels add overhead and error-prone complexity. Critical properties are then verified and proofed rather than relying on exhaustive testing (which never proves the absence of all errors).
The formal development of OpenComRTOS has also shown that such an integrated formalised approach results in serious improvements at several levels. The architecture is not only a lot more scalable and safe, it is also a lot more efficient. The code size is about 5 to 10 times smaller than a typically hand crafted implementation. Hence using formal techniques results not only in a more predictable development process, often the development costs will be lower (especially when taking into account traditional test and fix errors post development costs). It also results in more efficient systems, allowing using slower and cheaper processors with less memory and hence reducing power consumption. Just imagine a world where all embedded software (we forgo the desktop world for the time being) would be 5 times smaller and a lot more "trustworthy". The world would be very different, safer and greener at the same time. Contrary to popular belief, memory has not really got cheaper. Memory density in chips has increased, but still the gap between memory speed and processor speed remains in place. What's the benefit of using a 2 GHz processor if it needs power hungry caches (to give real-time wise unpredictable performance) and when cache misses occur, the performance penalty can be a factor of 200 to 300?
It is also our pleasure to announce that the best paper award of FM2009 was to Professor Raymond Boute (Making temporal logic calculational: a tool for unification and discovery). Prof. Boute was our scientific advisor during the formal development of OpenComRTOS and this award above all demonstrates how he can combine formal rigor with clear thinking about how formal thinking is part of the engineering process.
Attachment | Size |
---|---|
OpenComRTOS_A_Runtime_Environment_for_Interacting_Entities.pdf | 275.15 KB |
- Printer-friendly version
- Login to post comments