Formal Development of a Real-Time Kernel | Jacob Andersen, Mikael Buchholtz
| | Abstract | In this thesis we investigate how to formally develop a real-time kernel for reactive systems. We based our investigation on the ProCoS kernel development, which uses a semantics based, step-wise development approach. However, in the ProCoS kernel development real-time is not considered. We embark on our investigation by considering two different formalisms in which real-time semantics can be given. These are Duration Calculus and structural operational semantics, which is based on labelled transition systems. Concluding on these considerations we proceed by using structural operational semantics. We conduct a full kernel development by a specification of three development levels. The most abstract level describes the system as a number of CSP-like processes running in parallel. The most concrete development level describe a virtual machine, known as the kernel, which can execute the processes by switching execution among them. From the specification of the most concrete development level we have derived a sequential program. This program has been implemented for the RCX brick of the LEGO Mindstorms set. We discuss how to formalise a notion of correctness of the development based on implementation between labelled transition systems. Furthermore, we consider how to formally verify that the specifications are correct with regard to this notion of correctness. | | Keywords | kernel, real-time, formal methods, reactive systems, correctness, LEGO Mindstorms RCX brick | | Type | Master's thesis [Academic thesis] | | Year | 2001 Month February | | Publisher | Department of Information Technology | | Address | Richard Petersens Plads, Build. 322 | | Electronic version(s) | [ps] | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|