Title :
Integrating test and proof in the verifiable spark 2014 language using contracts and SMT solvers
Author_Institution :
AdaCore Inc., Lexington, MA, USA
Abstract :
Cost of testing greater than cost of development. 100/0 increase each year for avionics software (Boeing META Project). Uneven partitioning, uneven quality: 800/0 of errors traced to 200/0 of code. Need to reduce and focus the cost of testing. Formal methods might be the primary source of evidence for the satisfaction of many of the objectives concerned with development and verification.
Keywords :
aerospace computing; avionics; computability; contracts; formal languages; formal verification; program testing; SMT solvers; Verifiable Spark 2014 Language; avionics software; contracts; cost of development; cost of testing; cost reduction; formal methods; uneven partitioning; uneven quality; Aerospace electronics; Multicore processing; Software; Testing;
Conference_Titel :
Digital Avionics Systems Conference (DASC), 2013 IEEE/AIAA 32nd
Conference_Location :
East Syracuse, NY
Print_ISBN :
978-1-4799-1536-1
DOI :
10.1109/DASC.2013.6719720
