Formal verification of concurrent scheduling strategies using TLA

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationThe 13th International Conference on Parallel and Distributed Systems, ICPADS
Volume2
DOIs
Publication statusPublished - 2007
Event13th International Conference on Parallel and Distributed Systems - Hsinchu, Taiwan, Province of China
Duration: 5 Dec 20077 Dec 2007

Conference

Conference13th International Conference on Parallel and Distributed Systems
Abbreviated titleICPADS
CountryTaiwan, Province of China
CityHsinchu
Period5/12/077/12/07

Fingerprint

Temporal logic
Scheduling
Computer programming languages
Formal verification

Cite this

Grov, G., Michaelson, G., & Ireland, A. (2007). Formal verification of concurrent scheduling strategies using TLA. In The 13th International Conference on Parallel and Distributed Systems, ICPADS (Vol. 2) https://doi.org/10.1109/ICPADS.2007.4447839
Grov, Gudmund ; Michaelson, Greg ; Ireland, Andrew. / Formal verification of concurrent scheduling strategies using TLA. The 13th International Conference on Parallel and Distributed Systems, ICPADS. Vol. 2 2007.
@inproceedings{311f9c5a5bcb42d9bf8952cf880393cf,
title = "Formal verification of concurrent scheduling strategies using TLA",
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. {\circledC} 2007 IEEE.",
author = "Gudmund Grov and Greg Michaelson and Andrew Ireland",
year = "2007",
doi = "10.1109/ICPADS.2007.4447839",
language = "English",
isbn = "9781424418909",
volume = "2",
booktitle = "The 13th International Conference on Parallel and Distributed Systems, ICPADS",

}

Grov, G, Michaelson, G & Ireland, A 2007, Formal verification of concurrent scheduling strategies using TLA. in The 13th International Conference on Parallel and Distributed Systems, ICPADS. vol. 2, 13th International Conference on Parallel and Distributed Systems, Hsinchu, Taiwan, Province of China, 5/12/07. https://doi.org/10.1109/ICPADS.2007.4447839

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 proceedingConference 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 -

Grov G, Michaelson G, Ireland A. Formal verification of concurrent scheduling strategies using TLA. In The 13th International Conference on Parallel and Distributed Systems, ICPADS. Vol. 2. 2007 https://doi.org/10.1109/ICPADS.2007.4447839