Formal verification of concurrent scheduling strategies using TLA

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

3 Citations (Scopus)

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 Dive into the research topics of 'Formal verification of concurrent scheduling strategies using TLA'. Together they form a unique fingerprint.

Cite this