The importance of system properties such as correctness, reliability and dependability does not need any elaboration. The use of formal methods to ensure such properties in a mathematically rigorous and well established way in the area of protocol design. Specifically, model checking is a technique which is commonly used to verify specific correctness aspects of network protocols.
Verifying specific aspects of an abstract model does however not necessarily mean that the actual implementation of the protocol running on the real system is correct. Formal methods which apply to actual software also exist; for example, there are program verification tools which allow to formally prove the correctness of a given program against a specification. Despite their great potential for finding and eliminating software bugs, such tools are not currently employed widely in industrial software engineering. The main reasons are that they are still difficult to use, and that they are usually not able to deal with all features of real-world programming languages. However, these tools and techniques have matured significantly over the last decade, and applying them to realistic pieces of software is more and more becoming a possibility.
The world of miniature distributed systems is an interesting target for software verification, because the programs used in this context are (i) often safety critical, and (ii) of somewhat limited complexity. Verification is also made significantly more feasible when the targeted software is written in an abstract, hardware-independent language with a fixed semantics such as Java. A prime example for this are smart cards programmed in Java Card.
The software of wireless sensor networks has to our knowledge not yet been the target of intensive use of formal methods. Compared to Java Card software, verifying such software is much more challenging because of its larger size and its making use of more complex language features, such as concurrency, and a larger API. However, the use of Java as programming language makes Sun SPOT software much more accessible for formal verification than software on other sensor devices.
The present Diploma Thesis is performs a case study on the Squawk API implementation using the KeY tool. We formally specify and verify parts of that library.
To complement the present results, we plan to complement this effort with model checking to cover multi-threading aspects not suitable for program verification.