As computers are progressively invading every area of our life, a failure of a computer, electronic or electromechanical system may cause catastrophic injury or death to human beings. The safety critical applications such as aircraft or nuclear power station control system gain more attentions of software safety researchers. Current commercial programming languages cannot ensure that software is error free and consequently suggestions of safer programming languages play an important role in safety critical systems to ensure reliable software behavior. The C language is widely adopted for safety-critical systems. However, it is known that the C language is an unsuitable choice for safety-critical system since the C language includes several bad language features such as heavy use of pointers. The aim of this work is to define safe subset of the C language and translate the subset into the SPARK Ada so that we can verify the program’s safety using SPARK analysis tools. SPARK is a safe subset of Ada and have been successfully applied to high integrity system development. The C program translated into SPARK has the same integrity level as SPARK, and the program correctness can be verified by using Examiner which is a SPARK analysis tool. An elevator controller case study is presented and is used to demonstrate the potential use of our approach to implement a realistic system. We also developed a translator that automatically translates C code into SPARK in accordance with the translation rules.
