Protein matching using runtime verification

Abstract

Given that software systems form an integral part of our lives, they must be guaranteed to work correctly every time. The field of software verification has put forward several techniques but given the intractability of applying formal verification techniques on larger systems, the lack of coverage associated with testing and the need to verify a system in its own environment led to the introduction of runtime verification techniques. Runtime verification techniques verify the system as it is executing through the use of a monitor. Built through a system requirement specification, the monitor is executed with the underlying system to listen for appropriate events, trigger verification procedures and execute reparatory actions where needed. Additional statistics techniques enable the monitor to watch for indicators of failure while also enabling the specification of nonfunctional requirements such as system performance. We theorise that we can also use such techniques to provide extra functionality to the underlying system. Thus, apart from execution verification procedures. one can also use such techniques to provide additional logic to the system itself. The extra logic we chose to implement is that of a sequence alignment algorithm in the field of Bioinformatics. These algorithms compare sequences through alignment, that is, by finding any common similarities between the sequences content and by accepting any mutations which are believed to be evolutionary plausible. Such alignments are finally scored through appropriate scoring mechanisms and if they result to be significantly similar, they can be used to reveal previously unknown evidence of homology. To implement such logic. we need to make use of a runtime verification framework which is sufficiently expressive for our needs and also able to intuitively express statistics collection. We identify this framework to be Larva and its statistical extension LarvaStat. This framework is an event-based tool which uses Dynamic Automata with Timers and Events (DATEs) for the specification of the required logic. Apart from offering the definition of temporal aspects through timers, DATEs also allow the definition of contextual aspects so as to allow functionality to be executed both locally on a per monitored object bases and also globally for all the objects. Its statistical extension LarvaStat allows the framework to define addition statistics which are collection at runtime either at specific points in time or over interval durations. This thesis is primarily concerned with the implementation of two protein matching tools which take advantage of runtime verification techniques. The first tool will be an implementation of the Blast algorithm, one of the most popular sequence alignment algorithms available. The second tool will be implemented using simpler rules for protein matching which will trade off sensitivity for speed. The results obtained from both tools will be evaluated through the comparison with the results obtained by a third-party available BLAST implementation tool.