A language to support verification of embedded software

[摘要] ENGLISH ABSTRACT:Embedded computer systems form part of larger systems such as aircraft or chemical processingfacilities. Although testing and debugging of such systems are difficult, reliability is oftenessential. Development of embedded software can be simplified by an environment that limitsopportunities for making errors and provides facilities for detection of errors. We implementeda language and compiler that can serve as basis for such an experimental environment. Bothare designed to make verification of implementations feasible.Correctness and safety were given highest priority, but without sacrificing efficiency whereverpossible. The language is concurrent and includes measures for protecting the address spacesof concurrently running processes. This eliminates the need for expensive run-time memoryprotection and will benefit resource-strapped embedded systems. The target hardware isassumed to provide no special support for concurrency. The language is designed to besmall, simple and intuitive, and to promote compile-time detection of errors. Facilities forabstraction, such as modules and abstract data types support implementation and testing ofbigger systems.We have opted for model checking as verification technique, so our implementation languageis similar in design to a modelling language for a widely used model checker. Because ofthis, the implementation code can be used as input for a model checker. However, since thecompiler can still contain errors, there might be discrepancies between the implementationcode written in our language and the executable code produced by the compiler. Thereforewe are attempting to make verification of executable code feasible. To achieve this, ourcompiler generates code in a special format, comprising a transition system of uninterruptibleactions. The actions limit the scheduling points present in processes and reduce the differentinterleavings of process code possible in a concurrent system. Requirements that conventionalhardware places on this form of code are discussed, as well as how the format influencesefficiency and responsiveness.

[发布机构] Stellenbosch University