High-Integrity Multitasking in SPARK: Static Detection of Data Races and Locking Cycles
S. Tucker Taft, Florian Schanda, Yannick Moy · 2016
SPARK is a subset of Ada designed to enable formal verification. A new release of SPARK 2014, based on the Ada 2012 standard, incorporates support for multitasking, based on the Ravenscar Profile, which subsets the full Ada tasking model to a relatively static, single-level tasking model. This paper describes the safety requirements relating to multitasking in this version of SPARK, and the corresponding static checks performed by the SPARK 2014 toolset.