Name
Title | ||
|---|---|---|
High-Integrity Multitasking in SPARK: Static Detection of Data Races and Locking Cycles |
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1109/HASE.2016.54 | 2016 IEEE 17th International Symposium on High Assurance Systems Engineering (HASE) |
Keywords | Field | DocType |
formal verification,multitasking | Synchronization,Spark (mathematics),System recovery,Computer science,Ravenscar profile,Real-time computing,Human multitasking,Operating system,Embedded system,Formal verification | Conference |
ISSN | Citations | PageRank |
1530-2059 | 1 | 0.35 |
References | Authors | |
3 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| S. Tucker Taft | 1 | 50 | 14.12 |
| Florian Schanda | 2 | 16 | 3.20 |
| Yannick Moy | 3 | 69 | 9.25 |