Automated verification of code automatically generated from Simulink (R)
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. T...
| Yazar: | |
|---|---|
| Materyal Türü: | Journal article |
| Dil: | English |
| Baskı/Yayın Bilgisi: |
2013
|
| _version_ | 1826304638499946496 |
|---|---|
| author | O'Halloran, C |
| author_facet | O'Halloran, C |
| author_sort | O'Halloran, C |
| collection | OXFORD |
| description | 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. © 2012 Springer Science+Business Media New York. |
| first_indexed | 2024-03-07T06:20:50Z |
| format | Journal article |
| id | oxford-uuid:f2a8fd25-e2f8-4361-b240-7ce20844b6ac |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T06:20:50Z |
| publishDate | 2013 |
| record_format | dspace |
| spelling | oxford-uuid:f2a8fd25-e2f8-4361-b240-7ce20844b6ac2022-03-27T12:05:39ZAutomated verification of code automatically generated from Simulink (R)Journal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:f2a8fd25-e2f8-4361-b240-7ce20844b6acEnglishSymplectic Elements at Oxford2013O'Halloran, CThe 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. © 2012 Springer Science+Business Media New York. |
| spellingShingle | O'Halloran, C Automated verification of code automatically generated from Simulink (R) |
| title | Automated verification of code automatically generated from Simulink (R) |
| title_full | Automated verification of code automatically generated from Simulink (R) |
| title_fullStr | Automated verification of code automatically generated from Simulink (R) |
| title_full_unstemmed | Automated verification of code automatically generated from Simulink (R) |
| title_short | Automated verification of code automatically generated from Simulink (R) |
| title_sort | automated verification of code automatically generated from simulink r |
| work_keys_str_mv | AT ohalloranc automatedverificationofcodeautomaticallygeneratedfromsimulinkr |