Please use this identifier to cite or link to this item:
http://hdl.handle.net/11375/16234
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.advisor | Maibaum, Thomas | - |
dc.contributor.author | Demasi, Ramiro | - |
dc.date.accessioned | 2014-10-28T18:11:03Z | - |
dc.date.available | 2014-10-28T18:11:03Z | - |
dc.date.issued | 2014-11 | - |
dc.identifier.uri | http://hdl.handle.net/11375/16234 | - |
dc.description.abstract | This dissertation concentrates on the problem of synthesizing fault-tolerant components from specifications, i.e., the problem of automatically constructing a fault- tolerant component implementation from a logical specification of the component, and the system’s required level of fault-tolerance. In our approach, the logical specification of the component is given in dCTL-, a fragment of a branching time temporal logic with deontic operators, especially designed for fault-tolerant component specification. Deontic logics have proved to be useful for reasoning about legal and moral systems, where the situation is more or less similar to fault-tolerance: there exists a set of rules that states what the normal behaviours or scenarios are. Violations arise when these rules are not followed and, as a consequence, some actions must be performed to return to a normal or desirable state. As a black-box overview, our synthesis algorithm takes the component specification and a user-defined level of fault-tolerance (masking, nonmasking, or failsafe), and automatically determines whether a component with the required fault-tolerance is realizable. Moreover, if the answer is positive, then the algorithm produces such a fault-tolerant implementation. Our technique for synthesis is based on the use of (bi)simulation algorithms for capturing different fault-tolerance classes, and the extension of a synthesis algorithm for CTL to cope with dCTL- specifications. Some case studies are provided throughout this thesis to illustrate how the ideas described below can be applied in practice. Moreover, we have implemented a tool called dCTL Synthesizer (syntdctl) which was used to synthesize automatically well-known fault-tolerant examples. | en_US |
dc.title | Synthesizing Fault-Tolerant Programs from Deontic Logic Specifications | en_US |
dc.type | Thesis | en_US |
dc.contributor.department | Computing and Software | en_US |
dc.description.degreetype | Thesis | en_US |
dc.description.degree | Doctor of Philosophy (PhD) | en_US |
Appears in Collections: | Open Access Dissertations and Theses |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Demasi_Ramiro_A_finalsubmission201408_PhD.pdf | 1.44 MB | Adobe PDF | View/Open |
Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.