Open License Society ______Only software can be perfect

An industrial case: pitfalls and benefits of applying formal methods to the development of a network-centric RTOS 
Abstract. This paper describes a project to develop a network-centric RTOS from scratch using formal methods. The (initial) purposes of the project was to get acquainted with the use of formal methods for software engineering and to obtain a trustworthy RTOS as a component for building networked embedded systems. The work was done by a small, distributed team that had no prior experience on using formal methods and with a small budget. The outcome is that the use of formal methods is most useful as an architectural design method, more than as a formal verification of software code. The resulting software has many properties that were not anticipated at the beginning and would likely not have been achieved without the use of Formal Methods.
Full draft paper in attachment.
 
Visit the website of FM'08 here