Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/22747
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Cordina, Joseph | - |
dc.contributor.author | Fenech, Stephen | - |
dc.contributor.author | Pace, Gordon J. | - |
dc.date.accessioned | 2017-10-17T10:02:53Z | - |
dc.date.available | 2017-10-17T10:02:53Z | - |
dc.date.issued | 2007 | - |
dc.identifier.citation | Cordina, J., Fenech, S., & Pace, G. J. (2007). Model checking concurrent assembly algorithms. 5th Computer Science Annual Workshop (CSAW’07), Msida. 162-174. | en_GB |
dc.identifier.uri | https://www.um.edu.mt/library/oar//handle/123456789/22747 | - |
dc.description.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. | en_GB |
dc.language.iso | en | en_GB |
dc.publisher | University of Malta. Faculty of ICT | en_GB |
dc.rights | info:eu-repo/semantics/openAccess | en_GB |
dc.subject | CSP (Computer program language) | en_GB |
dc.subject | Modeling languages (Computer science) | en_GB |
dc.subject | Computer programs -- Verification | en_GB |
dc.subject | Computer multitasking | en_GB |
dc.subject | Assembly languages (Electronic computers) | en_GB |
dc.title | Model checking concurrent assembly algorithms | en_GB |
dc.type | conferenceObject | en_GB |
dc.rights.holder | The copyright of this work belongs to the author(s)/publisher. The rights of this work are as defined by the appropriate Copyright Legislation or as modified by any successive legislation. Users may access this work and can make use of the information contained in accordance with the Copyright Legislation provided that the author must be properly acknowledged. Further distribution or reproduction in any format is prohibited without the prior permission of the copyright holder. | en_GB |
dc.bibliographicCitation.conferencename | 5th Computer Science Annual Workshop (CSAW’07) | en_GB |
dc.bibliographicCitation.conferenceplace | Msida, Malta, 5-6/11/2007 | en_GB |
dc.description.reviewed | peer-reviewed | en_GB |
Appears in Collections: | Scholarly Works - FacICTCS |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
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.