Demonstrating Whiley on an Embedded System
Author(s). Matt Stevens.
Venue. Final Year Project (ENGR489) Thesis, Victoria University of Wellington, 2014.
Abstract. Developing and verifying the software for safety critical embedded systems can be difficult and expensive due to unique constraints, including limited RAM and minimalist operating systems. This report looks at Whiley, a verifying compiler, which is intended to improve the correctness of code on a variety of systems. For the first time, Whiley is explored in the embedded systems context to identify obstacles to becoming a practical tool for embedded systems programmers. The conclusion identifies three areas of work for the Whiley project; resolving memory management issues inherent in embedded systems, facilitating unbounded to bounded datatype conversions and improving the ability to determine bytecode context. The forth conclusion is to adopt the use of industry debugging tools, reflecting the difficulty of debugging an embedded system. This work built a Whiley to C compiler and using it, achieved demonstrating Whiley on an embedded system — the Bitcraze Crazyflie Quad-copter. Experiments conclude that the code automatically generated by the Whiley to C compiler, performs comparably to the original C code.