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.
|Title of host publication||The 13th International Conference on Parallel and Distributed Systems, ICPADS|
|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||13th International Conference on Parallel and Distributed Systems|
|Country/Territory||Taiwan, Province of China|
|Period||5/12/07 → 7/12/07|