Please use this identifier to cite or link to this item:
http://hdl.handle.net/11375/21046
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.advisor | Lawford, Mark | - |
dc.contributor.advisor | Parnas, David | - |
dc.contributor.author | Pantelic, Vera | - |
dc.date.accessioned | 2017-02-03T17:57:16Z | - |
dc.date.available | 2017-02-03T17:57:16Z | - |
dc.date.issued | 2005-12 | - |
dc.identifier.uri | http://hdl.handle.net/11375/21046 | - |
dc.description | Title: Inspection of Concurrent Systems: Combining Tables, Theorem Proving and Model Checking, Author: Vera Pantelic, Location: Thode | en_US |
dc.description.abstract | <p>A process for rigorous inspection of concurrent systems using tabular specification was developed and applied to the classic Readers/Writers concurrent program by Jin in [15]. The process involved rewriting the program into a table and then performing a manual "column-by-column" inspection for safety and clean completion properties. The key element in the process is obtaining an invariant strong enough to prove the properties of interest. This thesis presents partial automation of the proposed approach by combining theorem proving and model checking. Model checking is first used to validate a formal model of the system with a small, fixed number of concurrent process instances. The verification of the system for an arbitrary number of processes is then performed using theorem proving together with model checking on the earlier model to quickly validate potential invariants before they are used in the formal proof. This method was used to check the manual proof of the Readers/Writers problem given in [15], discovering several random and one systematic mistake of the proof. Then, a new, significantly automated proof was performed.</p> | en_US |
dc.language.iso | en | en_US |
dc.title | Inspection of Concurrent Systems: Combining Tables, Theorem Proving and Model Checking | en_US |
dc.type | Thesis | en_US |
dc.contributor.department | Computing and Software | en_US |
dc.description.degreetype | Thesis | en_US |
dc.description.degree | Master of Applied Science (MASc) | en_US |
Appears in Collections: | Digitized Open Access Dissertations and Theses |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Pantrlic_Vera_2005_12_master.pdf | Title: Inspection of Concurrent Systems: Combining Tables, Theorem Proving and Model Checking, Author: Vera Pantelic, Location: Thode | 2.87 MB | Adobe PDF | View/Open |
Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.