LF : a language for reliable embedded systems

[摘要] ENGLISH ABSTRACT:Computer-aided verification techniques, such as model checking, are often considered essentialto produce highly reliable software systems. Modern model checkers generally require models tobe written in eSP-like notations. Unfortunately, such systems are usually implemented usingconventional imperative programming languages. Translating the one paradigm into the other isa difficult and error prone process.If one were to program in a process-oriented language from the outset, the chasm between implementationand model could be bridged more readily. This would lead to more accurate modelsand ultimately more reliable software.This thesis covers the definition of a process-oriented language targeted specifically towards embeddedsystems and the implementation of a suitable compiler and run-time system.The language, LF, is for the most part an extension of the language Joyce, which was defined byBrinch Hansen. Both LF and Joyce have features which I believe make them easier to use thanother esp based languages such as occam. An example of this is a selective communicationprimitive which allows for both input and output guards which is not supported in occam.The efficiency of the implementation is important. The language was therefore designed to beexpressive, but constructs which are expensive to implement were avoided. Security, however, wasthe overriding consideration in the design of the language and runtime system.The compiler produces native code. Most other esp derived languages are either interpreted orexecute as tasks on host operating systems. Arguably this is because most implementations ofesp and derivations thereof are for academic purposes only. LF is intended to be an implementationlanguage.The performance of the implementation is evaluated in terms of practical metries such as thetime needed to complete communication operations and the average time needed to service aninterrupt.

[发布机构] Stellenbosch University