Warning: A non-numeric value encountered in /home/skepticats/www/www/thesis/pathconfig.php on line 2
No Subject - FM Thesis

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:

  1. The Gypsy Verification Environment, which is often used for security-related systems. It is (or was) endorsed by the National Computer Security Center and has a Pascal-based programming language and first-order predicate-calculus for an assertion language.
  2. The TCAS methodology (unnamed at time of publication). This is based on Statecharts and uses tables to illustratetransitions between states.
  3. The Hewlett-Packard Specification Language (HP-SL), which uses a typing system reminiscient of traditional programming language to describe systems. This is augmented by predicate logic and defived types using sets, sequences, and maps. This one appears to be mostly confined to HP.
  4. The Formal Development Methodology (FDM), which is a state machine-based approach that uses Ina Jo and Ina Mod for specification and program assertions. This is also supported by the National Computer Security Center.
  5. Occam/Communicating Sequential Processes (CSP), which I don't really get. Apparently it's a program transformation approach based on the idea of a process communicating with its environment. Occam is based on CSP and is the programming language used for Transputers.
  6. The Rigorous Approach to Industrial Software Engineering (RAISE). I didn't really get anything concrete about it from the description, other than that it evolved from VDM.
  7. Hoare Logics, which I already know all about.
  8. Z, which I've been reading all about lately.

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.

Add your comments #

A comment body is required. No HTML code allowed. URLs starting with http:// or ftp:// will be automatically converted to hyperlinks.