Well, in addition to a little more reading on Z, I finished the first volume of the International Formal Methods Survey today. The last 20 pages consisted of the rest of the formal methods overview, plus the initial survey given to the teams involved in the case studies. There's not really much to say about the survey, so I'll just give an overview of the methods.
I read about B, SCR (Software Cost Reduction), and Cleanroom yesterday. B uses an abstract machine approach with development through refinement. To me, it sounds pretty much like what I think of as a stereotypical formal method. SCR uses function tables and a "strongest postcondition" approach to exactly describe how the system state has changed. Lastely, Cleanroom is actually a hybrid development method where formal methods play a relatively small part. Appartently it uses some kind of assertion-based specification method on which I'm still a bit cloudy.
Today I covered the rest of the methods. These are:
The next step is to pick out a few case studies to look over in volume two. I don't think it's necessary to go over all the case studies, since I certainly won't use all of them. In particular, I can probably skip the exploratory group. However, I think I'll definitely want to look at CICS and SACEM, and probably TCAS, MGS, and Tektronix.
You can reply to this entry by leaving a comment below. You can send TrackBack pings to this URL. This entry accepts Pingbacks from other blogs. You can follow comments on this entry by subscribing to the RSS feed.