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.