Rafael Olaechea Velazco, PhD candidate
David R. Cheriton School of Computer Science
Software behavioural models, such as finite state machines, are used as an input to model checking tools to verify that software satisfies its requirements. As constructing such models by hand is time-consuming and error-prone, researchers have developed tools to automatically extract such models from systems’ execution traces.
In this seminar I will present GK-Tail+, which is an existing state-of-the-art tool that analyzes execution traces that consist of method calls annotated with values for their parameters. I discuss how effective the extracted models are in precisely representing the set of execution traces that the software can generate. Finally, I discuss the challenges associated with evaluating the quality of the extracted models.
200 University Avenue West
Waterloo, ON N2L 3G1