Formal Contracts for Runtime Verification Support in the Ada Programming Language

Abstract

Static Verification is not sufficient to cope with many of the challenges of modern and future generation real-time embedded systems: • state-explosion problem of model-checking; • limited automation in deductive reasoning, even with recent advances in SAT and SMT solvers. • Most of the data important to certify a real-time embedded system is related to extra-functional properties: • Duration of tasks; • Energy consumption; • Temperature management; • Other cyber-physical properties. • Unfortunately, most of the extra functional data is only available and verifiable during execution time.