CEN5015

Syllabus

Spring 2007

Ref #: 3790   Sec #: 301                       Meeting: 5:-6:15PM , MW, BBTA 208A, 01/08/2007 - 04/27/2007

Text: Notes, links & suggested texts

Instructor:  Dr. Riggs, BBTA 213, 850-412-7351, drkriggs at comcast.net

Course page: home.comcast.net/~drkriggs

Catalog description: CEN5016  SPEC SOFTWARE SYSTEM  Formal Methods of Software Engineering Prereq: COT3100 or equivalent. Exposes students to the use of specification that have well defined semantics.  Covers classes of specification models, including algebraic, state machines and model-theoretic approaches.  Reviews verification methods such as weakest pre-condition and functional correctness.

Topic Outline

Topic

Sources

Notes

Tools

Assignments

Logic,    Set Theory, models

Shapiro
  1. Logic
  2. Jape Proof Assistant
  3. Sets
  4. Typed logic
  5. Semantics
  6. Constraints (OCL)
  7. Theorem Provers

Jape

 

USE OCL?

1, 2

Formal Specification     & Verification

Gannon

 
8.             Axiomatic Verification 
9.             Algebraic Specification
  1. Functional Correctness
  2. Operational Semantics

NA

 

Hoare Logic

Gannon, TBA
  1. Axioms
  2. Examples

Jape

3, 4

Zed

TBA
  1. Elementary Z
  2. More Z by Eg
  3. Z-eves Theorem Proving!
  4. Z animation

Z-eves

Jaza

5,6

Alloy

TBA
  1. Alloy principles
  2. Alloy by examples

Alloy

7

Course Administration

 Grading: final grade = .4 exam average grade + .5 assignment average + .1 * participation grade   (scales adjusted to 100, 90, 80, etc.)

Exams: midterm (and final if not completely satisfied with results), possible quizzes over Z, Alloy as requied

      Assignments:

1.      Using the natural deduction logic (I2L.jt) in JAPE, prove (disprove) all the conjectures and classical conjectures (invalid conjectures) you can. Print your final proofs.  Bring a list of those you cannot prove to class. 

2.      Using the list of arguments handed out in class, prove or disprove each (if the argument is in ‘English’ you must formalize it first!)

3.      Using the Hoare logic (hoare.jt)  in JAPE, do as many of the supplied problems as possible. Bring your proofs and a list of your unanswered problems to class.

4.      Solve the problems handed out in class using JAPE and decide for each whether the program is correct or not.

5.      Duplicate the last Z example given in class

6.      Model the class problem (TBA) in Z. Extra credit given for finding and proving theorems interesting for the problem.

7.       Model your answer to 6 in Alloy

Policies: see standard policies