Software running on embedded systems is playing an increasingly important role in safetycritical and mission-critical applications. Formal documentation methods, like the Tabular Expressions invented by Parnas et al., avoid the ambiguities inherent in natural language by using mathematical notation. This allows the intended behavior of software to be precisely defined, reducing the number of errors that are caused by misleading documentation. Despite its shortcomings, software testing is considered an important part of software quality assurance. A fundamental assumption of software testing is the existence of some mechanism, which is called an oracle, that is able to determine whether the results of a test execution are correct. The oracle is often implemented by manually deriving the expected output from informal and possibly inconsistent documentation and then comparing it to the actual test results. This procedure is both time-consuming and error-prone. However, if a formal specification exists, it can be used to automatically evaluate the test results and determine the success or failure of a test execution. This thesis describes the design and implementation of a working prototype, which combines the use of Tabular Expressions and embedded-systems products developed by Ashling Microsystems Ltd. in a tool that is able to automatically execute function tests on a target embedded system, and evaluate their results using an existing formal specification of the tested function. In addition to testresult-evaluation, the tool is able to determine the specification-coverage of a given set of testcases on the basis of a formal specification, without depending on knowledge or even existence of program code. This allows measuring and improving test quality at any phase of a software project, even prior to implementation. A small trial application demonstrates the usefulness of the methods described in this work. Possible applications in projects and expected benefits are discussed. It is shown that using tests based on formal documentation enforces consistency between documentation and implementation, which greatly increases the value of such a documentation, especially to maintenance programmers. It is further argued that tools performing such tests help to reduce costs for software testing while improving test quality, and by doing so more than compensate the additional costs of creating formal specifications.