ITEM METADATA RECORD
Title: A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs (Een statisch verifieerbaar programmeermodel voor gelijktijdige objectgeoriënteerde programma's)
Other Titles: A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs
Authors: Jacobs, Bart
Issue Date: 15-Feb-2007
Abstract: Vele kritische computerprogramma's, met hoge betrouwbaarheidsvereisten, zijn gelijktijdig (m.a.w., de volgorde van de bewerkingen is niet volledig gespecificeerd) en zijn geschreven in op gedeeld geheugen gebaseerde gelijktijdige imperatieve programmeertalen. In de huidige stand van de technologie hebben programmeurs grote moeite met het afleveren van dergelijke programma's zonder programmeerfouten. Deze thesis stelt een aanpak voor die programmeurs kunnen gebruiken om te verifiëren dat een op gedeeld geheugen gebaseerd gelijktijdig imperatief programma, of een module van zo'n programma, vrij is van bepaalde vaak voorkomende programmeerfouten. Meer specifiek garandeert de aanpak de afwezigheid van dataraces en deadlocks en fouten tegen door de programmeur gespecificeerde correctheidscriteria. In deze aanpak annoteren programmeurs hun programma en voeren er dan een hulpprogramma op uit dat verificatiecondities genereert om te worden bewezen door een automatische stellingenbewijzer. De aanpak ondersteunt toestandsabstractie door middel van inspectormethodes, alsook onwijzigbare objecten en luie klasse-initialisatie. We hebben een prototype-implementatie ontwikkeld en met succes een aantal kleine programma's geverifieerd, en het verder werk nodig om de aanpak toepasbaar te maken in grote projecten geïdentificeerd.
ISBN: 978-90-5682-772-4
Publication status: published
KU Leuven publication type: TH
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
thesis.pdf Published 1162KbAdobe PDFView/Open

 


This item is licensed under a Creative Commons License
Creative Commons

All items in Lirias are protected by copyright, with all rights reserved.