An application of KLEE to aerospace industrial software

Resumen:

This work reports the initial experience of the authors on the application of KLEE to industrial aerospace software. The software consists of C mission code for the Attitude and Orbital Control System (AOCS) subsystem, together with the Simulink models from which it was automatically generated. We detail the characteristics of the software we analyzed, the workflow we created to apply KLEE in the context of Model-Driven Development, and the results and challenges we found.

Palabras Clave:

Aerospace software - Industrial experience - KLEE

Autor(es):

• Juan Francisco García {juanfrancisco.garcia@imdea.org}
  IMDEA Software Institute - Spain
  
• Daniel Jurjo {daniel.jurjo@imdea.org}
  IMDEA Software Institute - Spain
  
• Fernando Macías {fernando.macias@imdea.org}
  IMDEA Software Institute - Spain
  
• Jose F. Morales {josef.morales@imdea.org}
  IMDEA Software Research Institute - Spain
  
• Alessandra Gorla {alessandra.gorla@imdea.org}
  IMDEA Software Institute - Spain
  

Handle:

Descargas:

Este artículo tiene una licencia de uso CreativeCommons - Reconocimiento (by)

Descarga el artículo haciendo click aquí.

Ver la referencia en formato Bibtex