Abstract
There is a high demand for correctness for safety critical systems, often requiring the use of formal verification. Simple, well-understood scheduling strategies ease verification but are often very inefficient. In contrast, efficient concurrent schedulers are often complex and hard to reason about. This paper shows how the Temporal Logic of Action (TLA) can be used to formally reason about a well-understood scheduling strategy in the process of implementening a more efficient one. This is achieved by formally verifying that the efficient strategy preserves all properties, in particular the behaviour, of the simpler strategy. The approach is illustrated with the Hume programming language, which is based on concurrent rich automata. We introduce an efficient extension to the Hume scheduler, and prove that it preserves the behaviour of the standard Hume scheduler. © 2007 IEEE.
| Original language | English |
|---|---|
| Title of host publication | The 13th International Conference on Parallel and Distributed Systems, ICPADS |
| Volume | 2 |
| DOIs | |
| Publication status | Published - 2007 |
| Event | 13th International Conference on Parallel and Distributed Systems - Hsinchu, Taiwan, Province of China Duration: 5 Dec 2007 → 7 Dec 2007 |
Conference
| Conference | 13th International Conference on Parallel and Distributed Systems |
|---|---|
| Abbreviated title | ICPADS |
| Country | Taiwan, Province of China |
| City | Hsinchu |
| Period | 5/12/07 → 7/12/07 |
Fingerprint
Cite this
}
Formal verification of concurrent scheduling strategies using TLA. / Grov, Gudmund; Michaelson, Greg; Ireland, Andrew.
The 13th International Conference on Parallel and Distributed Systems, ICPADS. Vol. 2 2007.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
TY - GEN
T1 - Formal verification of concurrent scheduling strategies using TLA
AU - Grov, Gudmund
AU - Michaelson, Greg
AU - Ireland, Andrew
PY - 2007
Y1 - 2007
N2 - There is a high demand for correctness for safety critical systems, often requiring the use of formal verification. Simple, well-understood scheduling strategies ease verification but are often very inefficient. In contrast, efficient concurrent schedulers are often complex and hard to reason about. This paper shows how the Temporal Logic of Action (TLA) can be used to formally reason about a well-understood scheduling strategy in the process of implementening a more efficient one. This is achieved by formally verifying that the efficient strategy preserves all properties, in particular the behaviour, of the simpler strategy. The approach is illustrated with the Hume programming language, which is based on concurrent rich automata. We introduce an efficient extension to the Hume scheduler, and prove that it preserves the behaviour of the standard Hume scheduler. © 2007 IEEE.
AB - There is a high demand for correctness for safety critical systems, often requiring the use of formal verification. Simple, well-understood scheduling strategies ease verification but are often very inefficient. In contrast, efficient concurrent schedulers are often complex and hard to reason about. This paper shows how the Temporal Logic of Action (TLA) can be used to formally reason about a well-understood scheduling strategy in the process of implementening a more efficient one. This is achieved by formally verifying that the efficient strategy preserves all properties, in particular the behaviour, of the simpler strategy. The approach is illustrated with the Hume programming language, which is based on concurrent rich automata. We introduce an efficient extension to the Hume scheduler, and prove that it preserves the behaviour of the standard Hume scheduler. © 2007 IEEE.
UR - http://www.scopus.com/inward/record.url?scp=48049088769&partnerID=8YFLogxK
U2 - 10.1109/ICPADS.2007.4447839
DO - 10.1109/ICPADS.2007.4447839
M3 - Conference contribution
SN - 9781424418909
VL - 2
BT - The 13th International Conference on Parallel and Distributed Systems, ICPADS
ER -