Grijincu, Daniela (2013) Source Code Matching for Reuse of Formal Specifications. Masters thesis, National University of Ireland Maynooth.

Download (2MB)

Abstract

Although Software Verification technology is rapidly advancing, the process of formally specifying the intended behaviour of a program can still be difficult and time consuming as the program increases in size and complexity. In this project we focus on the source code matching module of Arís (Analogical Reasoning for reuse of Implementation & Specification) platform in which we aim to increase the number of verified programs by reducing the effort of writing specifications. Our approach promotes the advantages of code reuse and the possibility of transferring specifications between similar implementations. In order to effectively compare two source code files we represent them using Conceptual Graphs that allow us to explore the semantic content of the code while also analysing its structural properties using graph-based techniques. For comparing two conceptual graphs, we propose to use an incremental matching algorithm based on IAM (the Incremental Analogy Machine (Keane, et al., 1994)) and find the best mapping between isomorphic (exact matches) or homomorphic (non-identical) sub-graphs. We further develop analogical inferences from the acquired mapping using the CWSG (Copy With Substitution and Generation) algorithm for pattern completion and generate new specifications into our target/problem code. Finally, we present our evaluation and show that between structurally similar programs, the formal specifications can be fully transferred and successfully verified. Our overall results are very encouraging and clearly show the potential of reusing formal specifications in creating more dependable software systems.

Item Type:	Thesis (Masters)
Additional Information:	Taught Masters Thesis for the Erasmus Mundus MSc in Dependable Software Systems
Keywords:	Source Code Matching; Reuse of Formal Specifications;
Academic Unit:	Faculty of Science and Engineering > Computer Science
Item ID:	4556
Depositing User:	IR eTheses
Date Deposited:	07 Oct 2013 16:10
URI:
Use Licence:	This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

Repository Staff Only(login required)

Item control page

Downloads

Origin of downloads