This dissertation attempts to make a contribution within the fields of distributed systems, security,
and formal verification. We provide a way to formally assess the impact of a given change in
three different contexts. We have developed a logic based on Lewiss Counterfactual Logic. First
we show how our approach is applied to a standard sequential programming setting. Then, we
show how a modified version of the logic can be used in the context of reactive systems and sensor
networks. Last but not least we show how this logic can be used in the context of security systems.
Traditionally, change impact analysis has been viewed as an area in traditional software engineering.
Software artifacts (source code, usually) are modified in response to a change in user
requirements. Aside from making sure that the changes are inherently correct (testing and verification),
programmers (software engineers) need to make sure that the introduced changes are
coherent with those parts of the systems that were not affected by the artifact modification. The
latter is generally achieved by establishing a dependency relation between software artifacts. In
rough lines, the process of change management consists of projecting the transitive closure of the
this dependency relation based on the set of artifacts that have actually changed and assessing how
the related artifacts changed.
The latter description of the traditional change management process generally occurs after the
affected artifacts are changed. Undesired secondary effects are usually found during the testing
phase after the changes have been incorporated. In cases when there is certain level of criticality,
there is always a division between production and development environments. Change management
(either automatic, tool driven, or completely manually done) can introduce extraneous defects
into any of the changed software life-cycle artifacts. The testing phase tries to eradicate a
relatively large portion of the undesired defects introduced by change. However, traditional testing
techniques are limited by their coverage strength. Therefore, even when maximum coverage is
guaranteed there is always the non-zero probability of having secondary effects prior to a change.
| Identifer | oai:union.ndltd.org:LSU/oai:etd.lsu.edu:etd-10242012-153450 |
| Date | 31 October 2012 |
| Creators | Peralta, Manuel Alfonso |
| Contributors | Sabliov, Christina, Busch, Konstantin, Karki, Bijaya, Mukhopadhyay, Supratik, Keiser, Harmut |
| Publisher | LSU |
| Source Sets | Louisiana State University |
| Language | English |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | http://etd.lsu.edu/docs/available/etd-10242012-153450/ |
| Rights | unrestricted, I hereby certify that, if appropriate, I have obtained and attached herein a written permission statement from the owner(s) of each third party copyrighted matter to be included in my thesis, dissertation, or project report, allowing distribution as specified below. I certify that the version I submitted is the same as that approved by my advisory committee. I hereby grant to LSU or its agents the non-exclusive license to archive and make accessible, under the conditions specified below and in appropriate University policies, my thesis, dissertation, or project report in whole or in part in all forms of media, now or hereafter known. I retain all other ownership rights to the copyright of the thesis, dissertation or project report. I also retain the right to use in future works (such as articles or books) all or part of this thesis, dissertation, or project report. |
Page generated in 0.0019 seconds