Automated verification of code automatically generated from Simulink®

摘要

The CLawZ toolset independently and automatically proves the correctness of code automatically generated by a commercial auto-code generator for the Simulink® modelling language. The use of formal methods is invisible to the user and it has been shown to lead to faster development of correct code. The CLawZ toolset has been continually developed and used for over a decade to prove the correctness of embedded real time safety critical software for Eurofighter Typhoon. The only requirement on the commercial auto-coder is that it provides traceability information between the signal wires in a Simulink® model and the program variables that implement them.