Please use this identifier to cite or link to this item:
|Title:||Model checking concurrent assembly algorithms|
Pace, Gordon J.
|Keywords:||CSP (Computer program language)|
Modeling languages (Computer science)
Computer programs -- Verification
Assembly languages (Electronic computers)
|Publisher:||University of Malta. Faculty of ICT|
|Citation:||Cordina, J., Fenech, S., & Pace, G. J. (2007). Model checking concurrent assembly algorithms. 5th Computer Science Annual Workshop (CSAW’07), Msida. 162-174.|
|Abstract:||Model checking has been used in various domains, to enable automatic verification of properties for a given model. Especially in cases when the correctness of the the model is not evident due to the complex nature of the description, model checking can be an indispensable tool. One such domain is the use of concurrent assembly algorithms for lowlevel synchronisation, which can be notoriously difficult to check their correctness or even test. In this paper we look at this domain, and explore the use of model-checking in verifying a number of such algorithms, such as barrier synchronisation and wait-free CSP channel communication. We tackle the state explosion problem inherent in model checking by making use of abstraction techniques to remove rendundant information in the the model, and partial-order techniques to remove redundant interleavings of actions. Finally, we also investigate the use of structural induction to reason about families of systems of arbitrary size. Making use of symmetry and induction, we verify algorithms with an unbounded number of identical participating tasks.|
|Appears in Collections:||Scholarly Works - FacICTCS|
Files in This Item:
|Proceedings of CSAW’07 - A16.pdf||154.08 kB||Adobe PDF||View/Open|
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.