The FLAVERS Tutorial

This summer I worked at the University of Massachusetts at Amherst for Lori Clarke in LASER (Laboratory for Advanced Software Engineering Research). My job was to learn to use FLAVERS (Flow Analysis for Verification of Systems) and then figure out how to teach other people to use it. The project started out being just about FLAVERS itself. However, many of the things that make FLAVERS an unintuitive system to use are not native to the program itself, but the building blocks the program depends upon. An extended Regular Expressions syntax, Finite State Automata, etc. must all be understood before a user can even begin to use the program for system analysis. Because I came into the game with no background in these topics, the project's scope quickly expanded to include them, and the tutorial did as well.

You can view the tutorial in full here.

What I accomplished

project ended up being an important improvement and expansion to the existing FLAVERS documentation. The previous tutorial was far out of date and limited in its scope. No source had previously taken a user step-by-step through initializing a software system in FLAVERS, building properties to test the system on, writing constraints to refine the analysis, and interpreting analysis results. The tutorial we built this summer does all of these thing for three separate software systems and also covers the full extended regular expresions syntax and using FLAVERS' FSA editor to generate finite state automata to be used as properties and constraints. Where a beginner could not realistically learn to use FLAVERS on his own before, he has a much better head-start now. Writing the tutorial had a number of side-benefits. Coming from outside the LASER lab and the field of research, I was able to offer a lot of suggestions for the FLAVERS user interface that made it clearer and more intuitive. I also learned an awfully great deal about the theory behind software verification and analysis, going from drowning in an acronym sauce at the beginning to swimming along fairly easily by August. What remains to be done

FLAVERS incorporates a couple of features I was not able (due to time constraints) to cover in my tutorial, including a graphical path viewer that allows the user to follow a program trace step-by-step in a graphical manner. Also, the installation procedure is still very user-specific and was tough to document well. Had I had more time, I hoped to streamline and generalize this process. Hopefully, the tutorial is in such a state that it will be easy for other lab members to maintain and expand upon so that its development can continue since I've left.