. Kris Hauman

Weekly Project Journal

Dates of Mentorship: 6-3-02 to 8-9-02

week1       week2       week3       week4       week5
      week6       week7       week8       week9       week10      

See the Project section for a summary of what I'm doing.

Week One:

The first week on the job was enjoyable but also a little discouraging because I often didn't feel like I knew what I was doing. However, this lab has a relaxed, friendly atmosphere, so I feel pretty comfortable about doing the best I can and not stressing about all the things I don't know.

On the first day, Heather explained some about FLAVERS. She drew pictures of control flow and trace flow graphs (CFGs & TFGs), which I haven't dealt with before. I also learned what a finite state automaton is. I've been wishing I'd already taken Theory of Computation where I'll learn that stuff, but no one expects me to already know it.

I spent the first two days reading these papers:
FLAVERS: a Finite State Verification Technique for Software Systems
by Jamieson Cobleigh, Lori Clarke, and Leon Osterweil

The Right Algorithm at the Right Time: Comparing Data Flow Analysis Algorithms for Finite State Verification
by Jamieson Cobleigh, Lori Clarke, and Leon Osterweil

I didn't spend as much time on the second one since it wasn't as relevant to my project. The papers and a FLAVERS demo from Heather helped me to understand better what I'd be doing. It seems to be taking a while for it all to sink in.

As I understand so far, my project will involve saving FLAVERS users a little time when they're trying to determine if a counter-example is the real thing or if it can be ignored because it isn't really executable. The ones I'll deal with involve concurrent systems. I'll try to automate some of the choosing of " feasibility constraints ", specifically the ones called task automata. A task automaton ensures that nothing in that task happens out of order in all paths through the TFG considered in the analysis. The user now has to manually choose TA constraints to run FLAVERS with the more accurate, larger (and less efficient) graphs in order to determine if the violation of the property is due to a feasible path. --(if the counter-example is real).

I spent some time configuring things to be able to run java in the shell and emacs. I installed the JDEE (java development environment for emacs), which can take a while if you've never done it before. I had fun though, because it was the first time I'd ever installed it without any help. I'm finally remembering all the classpath stuff.

During the middle of the week I read some of the FLAVERS tutorial and played around with the FLAVERS system. Then Heather started giving me little programming assignments for me to become familiar with the LASER API and gain better understanding of how FLAVERS works.

The first program involved reading in a property and a TFG, then printing out the alphabets of each one. The alphabet is the set of labels (names of events) used in the property FSA and the TFG. Doing this allowed me to see what classes and methods are available, and also reinforced the meaning of all the new vocabulary.

Next, I wrote a program that reads in a property and a TFG and gives a list of the tasks in the TFG that are related to the property. A task is related to the property if their alphabets intersect, meaning that they have one or more of the same events. This could be helpful because it makes sense to have TA for a task that is relevant to the property that's being verified. For example, when trying to verify that the dining philosophers philosopher-1 and philosopher-2 don't eat at the same time because they're seated beside each other, it makes sense to have a TA for philosopher-1 and philosopher-2. This might be obvious to the user without a program suggesting those TA, and the program doesn't suggest any other necessary TA that unrelated to the property. So this TASuggestion class may or may not be extremely useful (I'm not sure yet), but writing it did help me understand FLAVERS and the project better.

Each week there are two meetings I attend in a small conference room with an oval wooden table that takes up the whole room. On Mondays the analysis-group meets (about 8 people), and everyone describes what they've been working on. The LASER meetings are on Fridays (analysis-group and process-group), filling up the conference room with approximately 20 people. However, we won't have another LASER meeting for the next two weeks since Lori Clarke will be in Japan.

Week Two:

I was feeling more comfortable in the LASER lab at the beginning of this week, after having gotten to know everyone better during lunches together. Most days we walk to the cafeteria on campus, but occasionally we go into downtown Amherst. The hours people work are very flexible, they don't " clock-in " and " clock-out, " but work on schedules that are convenient to them. It's a nice change from working at restaurants.

I got feedback from TASuggestion.java, made some changes, then tested it by comparing the trace output to a .dot graph in their program called Dotty.

I learned something new about java in the process. When running java, I can type this on the command line:
java -Dwhatever=[string] Tmp
Then, within the class Tmp, I can do:
String s = System.getProperty("whatever");
where s equals [string] given on command line.
Cool, I never heard of that.

I began comparing the task automata my program suggests with what TA is really needed to verify the property. This is to determine if finding all property-related tasks is helpful when the user is choosing constraints to deal with a counter-example.

I started creating this website after reading on the CRA-W site that I should send Nancy Amato the URL for it by the end of the second week of the project. I have fun writing, and it's helped me to clear up some fuzziness about FLAVERS and the project. Heather gave a talk on FLAVERS, which also helped.

Towards the end of the week, I began a new program that Heather thought would be good for learning about the PathFeasibility portion of FLAVERS. PathFeasibility determines if a path through a TFG is feasible in regards to any given constraints. I began writing TAFeasibility, which would basically do the same thing, except the path to be tested would be entered as standard-input. I haven't finished testing TAFeasibility yet.

Week Three:

The weeks here seem to be passing quickly. I started this week off by copying into my notebook all the loose notes I had floating around. --In the process I got to review everything I've learned, painting a clearer picture. I finished testing the TAFeasibility class which gave me a good understanding of PathFeasibility. I also got the hang of looking at the .dot files of TFGs and TA using the Dotty tool.

I worked more on comparing the property-related tasks suggested by the TA Suggestion program with examples, to see how useful the suggestions are, but haven't gotten too far with this yet.

I added other methods to the TaSuggestion class. One finds all the tasks in a TFG that are related to a particular constraint, which was basically the same as finding the property-related tasks. Another method finds all the tasks in a TFG that communicate with a given task.

The task names given by the getCommunicationRelatedTasks method are ranked in descending order from the largest to smallest values of the number of times the task communicated with the parameter task. I wasn't sure at first of the best way to store the names of the related tasks with their communication-frequency-counters.

I decided to have an inner class called TaskCommCount (for lack of a better name) that stores the name of a task and a counter and allows the counter to be incremented. For each task in the TFG that is found to communicate with the parameter task, a TaskCommCount object is created and put into a hashtable. So the getCommunicationRelatedTasks method can quickly find out if a task is already in the list. If it is, its counter is incremented; if not, it is put in there with the key being the task name and the value being the TaskCommCount object.

The method only needs to sort the tasks when it's completely done adding tasks. After adding is complete, all TaskCommCounts (hashtable values) are enumerated over and each one is inserted into its sorted place in an array.

I know this isn't the best way to do it, but my sorting algorithm was like this:

int currentIndex = 0;
int numArrayItems = 0;
rankedTasks is array for sorted tasks
while there's another TaskCommCount in the unsorted list {
  get the TaskCommCount
  while (currentIndex != 0) {
     if rankedTasks[currentIndex - 1] has a smaller count value
     than rankedTasks[currentIndex],
       copy rankedTasks[currentIndex - 1] to
       rankedTasks[currentIndex] and decrement currentIndex.
     otherwise, break.
  } end of loop to move items over to find right spot.
  rankedTasks[currentIndex] = taskCommCount;
  currentIndex = ++numArrayItems;
} end of ranking loop.

I should probably use a sort method of java.util.Arrays instead.

I spent some time testing the new TASuggestion methods, then got some feedback from Heather which I can look at to improve the program next week. I also worked on the this website a little.

Also this week, I played around with the PathViz tool to help Heather test it. She's getting ready for a demo in July, in which many of the LASER lab people will travel to Baltimore to show their grant-givers (DARPA) what progress they've made in their research.

The PathViz tool runs the find-path algorithm; it's given a text file with the property and TFG information, then looks for a counterexample (a path through the TFG in which the property is violated). If a counterexample is found, a GUI pops up that shows that path. A FSA panel shows the property, and the source code and a list of the events in the path are shown. The user can then execute, or step through the path. During the steps, the active line in the source code is highlighted and the current state in the FSA is turned green. As soon as the property is violated, the background of FSA changes color. After learning how it worked, I wrote some comments about how the GUI could be better.

On Friday I went to an INCA (Inequality Necessary Condition Analyzer) demo. INCA is a FSV tool like FLAVERS. Instead of using TFGs, INCA uses integer linear programming problems to describe how the property can be violated, then verifies the property by using a commercial program such as CPLEX to solve the linear programming problem. Though they use very different methods of verifying properties, both INCA and FLAVERS trade the accuracy of the model of the system for the ability to verify concurrent systems with numerous possible states.

All in all, I had a good week; maybe my best yet. The better I understand what I'm doing, the more fun I seem to have.

Week Four:

This week was ok, but not as fun as last week-- maybe because there was less programming and more not-sure-what-direction-to-take-researching.

I changed the sorting method I mentioned above to use Arrays.sort. Arrays.sort takes a Comparator to determine how it's sorted, so I passed it an anonymous inner class Comparator. Its compare method says that one TaskCommCount comes before another if its count is larger.

  Arrays.sort(this.rankedTasks, new Comparator() {
  public int compare(Object o1, Object o2) {
    int count1 = ((TaskCommCount) o1).getCount();
    int count2 = ((TaskCommCount) o2).getCount();
    if (count1 == count2)
      return 0;
      return (count1 > count2) ? -1 : 1;

Lori Clarke returned from Japan, so we met to discuss my project. She summarized the high-level ideas of what I'm doing, which helped.

I've still been trying to figure out if knowing the property-related, constraint-related, and communication-related tasks is helpful in suggesting what TA are needed to verify a property. I've mostly just been collecting data and thinking about how it would be possible to predict what TA is needed.

Collecting data involves running a Perl script that finds a counter-example in some example, running the TASuggestion, and sometimes finding the minimum TA needed to verify the property if that information is not already available. Then I compare what tasks TASuggestion listed with what TA were needed to get conclusive results. I'm using the system examples like atm, elevator, dining philosophers, reader-writer, producer-consumer, etc.

Collecting data got a bit tedious and I was thinking of how a Perl script could help with it, if only I knew Perl. I must learn it one day!

After collecting data for all the examples, I can start looking it over again and come up with possible approaches of making good predictions.

On Friday, a group of 13 LASER people ate lunch at Judy's restaurant downtown, so that was fun. Friday also brought disappointment when I accidentally missed the LASER meeting. I thought it was at 3:30, and didn't get the usual meeting-reminder email. I was in the restroom when everyone left for the meeting at 2:30, and by the time I figured it out, I felt it was too late to go in. Oh well.

Week Five:

This was a very quiet and short week. It was quiet because the lab is down a person (a graduate student, Matt, graduated), and Rachel, Erin, Sandy, Lori, and others went to Baltimore for their demonstration to DARPA. So very few people have been in LASER this week. The week was short because we're not working Thursday, July 4th, or Friday. I'm using that free time to go back to New Hampshire's White Mountains, this time for a hiking/camping trip.

The three days of this work-week were spent analyzing data collected from examples about what TA are needed, compared to what TA are property-related, constraint-related, and communication-related. I'm still trying to come up with possible ways of predicting what TA are needed, and how to fit some of that automation into the FLAVERS system.

I admit that this week of collecting/analyzing data and having nothing to program was not my favorite. I spent a little time looking at other DMP participants' websites for inspiration.

Heather met with me Wednesday to describe where my research might be heading next, and gave me a little program to write. So it looks like next week will be more fun.

Week Six:

The week started out with writing the TATermination program, which determines if a TA can terminate. A TA can terminate if its accepting state can be reached on a valid path from its start state. So I wrote a method that recursively searches for a path from the initial state to an accepting state, and returns true if such a path is found. TA that can't terminate will cause the verification algorithm to fail.

On Tuesday, I had fun becoming better acquainted with Lori, as she took me out to lunch. Tuesday was also my father-in-law's birthday, so Bruce and I visited him in CT (almost 2 hours from our place).

Lori, Heather, and I met to discuss my project. George (another professor involved with LASER) also joined us. I got some guidance about what direction to go in next, which I very much appreciated. I've noticed that it's much easier to be given assignments, as in class, than to come up with my own assignments. I find it harder to motivate myself if I don't have a clear, written out description of what I'm supposed to do. Maybe I'm just feeling lazy because it's summer.

At our meeting, I described the observations I'd made about how close the property-related, communication-related, or constraint-related tasks come to what TA are needed to verify a system's property. Based on those observations, I'll now experiment some and collect more information. I'll write some programs this time to automate some of that data collection.

For example, one thing I'll look at is the analysis results, run-time, and TA used in an example that includes all of the property-related TA. I'll then compare that information to the same example with only the TA needed to verify the property included. The purpose of doing this is to see if it's worth it to automatically include, or suggest, certain TA before the user does the first analysis. Also, which certain TA should be suggested? Does including many unneeded TA waste too much time?

Also this week, technician Rob replaced the video card on the computer I'm using, so I no longer have pink dotted lines running down the screen. They didn't bother me much, but I don't miss them.

Only 4 weeks left! I'm kinda looking forward to getting back to WCU for a new semester.

Week Seven:

I started writing some programs that would help to collect more information about the usefulness of the TASuggestion methods. This has been a very fun week of programming.

Lori suggested last week what information I should collect. I will compare the analysis-runtime, the TA used, and verification results of analysis problems that include:

  • the minimum TA needed for property verification
  • certain TA that are predicted to be needed
For example, I'll run the verification on the elevator example that only uses the minimum of TA needed to verify the property. I'll also run the verification on the elevator example that includes only TA that are property-related. By comparing these results, I can get a better idea of how close the property-related, constraint-related, or communication-related tasks come to the combination needed for property verification. The runtimes will indicate if it's too costly to include the TA that are related somehow but not needed for property verification.

The first program I'm working on, AppendTASuggested, adds certain TA to a copy of an analysis problem test case file. Which TA are added depends on the choice of TASuggestion methods that is given as input. For example, all property-related TA might be added to the file, all constraint-related TA, or both. This program will get the test case file ready for analysis, rather than doing it manually as I did when collecting data before.

I started writing this program by modifying an already existing program that builds the analysis problem (such as the TFG and property). Sometimes I had trouble figuring out the best way to organize the code. I should probably think about organization on paper first, rather than to write code and keep changing it around.

Rachel gave a demo on PROPEL (Property Elucidator), which I attended. PROPEL helps FLAVERS users express properties in a precise and accessible way. Properties can be expressed as FSA (finite state automata) and DNL (disciplined natural language).

Heather showed me how to check source files into CVS. It was really neat to learn about that handy tool. Before submitting the TASuggestion program, I made those source files part of a package. I hadn't done much with creating new packages before, but it's easy.

At the end of the week, I created a short Power Point presentation for Matt Dwyer's visit next week. Matt is a former student of Lori's, who started the FLAVERS system. Lori wants me to describe to Matt what I've been working on. Though I get a little stressed about having to speak to a group, people here make me feel comfortable enough to handle a short presentation.

Week Eight:

Wow, this week went by quick. I stayed very busy the whole week and will likely remain busy for my last 2 weeks here.

At the beginning of the week, I listened to presentations by Shangzhu and Isha (2 of the female graduate students in LASER), Jianbin, Ricky, Heather, and Matt Dwyer. Matt is a professor at Kansas State. I gave my short Power-Point presentation about predicting what TA are needed for property verification. I guess it went well, (Lori and Heather were nice enough to say so), though it's hard for me to tell since I was nervous. I'd much rather write a report than give an oral presentation.

Matt spoke about a tool that generates code for synchronization from specified invariants. So the synchronization coding lies at a high level, and the specified invariants are independent of platform, language, or synchronization primitives. Synchronization patterns aid in the invariant specification. For example, Exclusion(R1, R2) means mutual exclusion is needed in those regions.

I spent all week writing programs that will run analyses and gather information for me. After finishing the AppendTASuggested program I started last week, I wrote CompareTAUsed. This program outputs a file that describes the differences in the file that includes the minimum TA and the file that includes the predicted TA. For example, it will say whether the predicted TA make up a superset or subset of the needed TA, or neither.

Another program I wrote is NoTAFileMaker, which just makes a copy of the file consisting of the minimum TA needed and strips all the TA out of the copy. This file with no TA is needed for the AppendTASuggested program to start from when adding TA. I probably haven't made it clear what input files I'm talking about. An analysis problem example, such as the dining philosophers example, has input files used to generate the TFG, TA, property, and other stuff needed to perform the system analysis which determines if the property holds for all paths through the TFG.

The program I finished up at the end of the week generates all the comparison files for each experiment. So I can give it the name of a test case file and it will compare its TA to: a file that includes all the property-related TA; a file that includes all the constraint-related TA; a file that includes all the property and communication-related TA; and other files with certain predicted TA which may or may not turn out to be a good prediction.

So, this week was full of programming, debugging, documenting, note-taking, and more programming. I enjoyed it. When I met with Lori this week, she told me I should start working on another Power Point presentation that describes the entire project. The slides will form an outline from which I can write a report for LASER about the research I've done. The report might be useful when someone else here looks into how to automate choosing TA.

Week Nine:

As the end of my mentorship gets closer, the excitement rises. There's lots of loose ends to tie up before I head back to NC for another great semester.

At the beginning of the week I modified a Perl script to generate all of the test case files with predicted TA before performing the analysis on all input files. I had a little help in doing this, since I don't know Perl. I was happy to be using Perl, since programming with it is so much quicker than Java sometimes.

Before running the script that would perform all the analyses, I had to keep doing little things like updating the JDK. I had a few false starts of running the experiments, because of slow machines and platform problems. The script will run over the weekend and hopefully all the data will be successfully collected when I return to work next week.

Other than getting the script started, I wrote a program to gather up all of the compare files (generated by CompareTAUsed, mentioned last week) and dump all of that information into a table-formatted file that can be read by Excel. When Lori, Heather, and I met, we decided what information should be shown in the table.

I've also been working on the presentation and report. I felt a little overwhelmed and procrastinated a bit during the middle of the week. But when my confidence picked up, so did my motivation.

Week Ten:

This was the hardest week of the entire mentorship. I spent long hours each day trying to finish everything up and get my final presentation ready. Thursday was the most exciting day of the week. That's when a group of LASER people took me out to lunch, I gave my final Power Point presentation at the LASER meeting, and we went to a LASER party at Lori's that evening.

I dreaded giving the presentation, but it ended up being not as painful as I imagined. When I was going through the slides, Lori sometimes elaborated on what I said, which I really appreciated. I didn't feel as nervous since I wasn't the only one talking.

An undergraduate in the lab, Matt, decided he would pick up the TA prediction project where I left off. So I tried hard to leave all of my code and documents in a good state.

Analyzing the results from the experiments required lots of time that I was quickly running out of. The generated tables contained all the measurements, but I then needed perl scripts to make observations about those measurements. For example, I needed to know the number of conclusive results each prediction approach had. Some spreadsheet programs might have tools for searching for certain things in the table, and counting the number of rows that have certain data in certain columns, but I don't know how to do it. I don't know perl well enough to do it either, but fortunately I have Bruce to help me with that.

Though I didn't have time to analyze the results much, I was able to make a bar graph for the presentation. It showed the percent of conclusive results for each prediciton approach. I left Matt documents describing many factors that probably caused those percentages to be inaccurate, so I can't tell you which prediction approach worked the best.

I must say, LASER has been a great environment for learning. The people in this lab are friendly, supportive, and fun. Lori has been a warm and encouraging mentor. This has been a summer I'll never forget.