[ IS | JAIST ]
http://www.jaist.ac.jp/~kokichi/class/i613-1312/

---

Web Page for the Course of Lectures:

Algebraic Formal Methods (i613)

5 December 2013 (Thur.) - 6 February 2014 (Thur.)
at I-2 Lecture Room of JAIST-IS

Lecturers:  FUTATSUGI,Kokichi + OGATA,Kazuhiro
Invited Lecturers:  GAINA,Daniel + NAKAMURA,Masaki + PREINING,Norbert + ZHANG,Min
      (Send e-mail to FUTATSUGI ＋ OGATA for queries)

---

Goal of the Course

To obtain (1) the ability of formalizing requirement or design specifications for system developments in formal specifications based on the formal systems like sets, functions/maps, and algebras, and (2) the ability of analysing and/or verifying the obtained formal specifications.

Syllabus of the Course

---

Schedule and Materials

1. [Dec.05 (Thur.) 11:00-12:30]  Basics of CafeOBJ and Peano Style Natural Numbers (Futatsugi)
   
   Lecture Note 01   Lecture Note 01a   CafeOBJ Code 01   Sample answers to excercise 01
2. [Dec.10 (Tue.)  09:20-10:50]  Parameterized Modules and Generic List Structure (Futatsugi)
   
   Lecture Note 02   CafeOBJ Code 02   Sample answers to excercise 02
3. [Dec.12 (Thur.) 11:00-12:30]  Constructor-based Inductive Theorem Prover (CITP) (1) (Gaina)
   
   Lecture Note 03
4. [Dec.17 (Tue.)  09:20-10:50]  Inference with Rewriting Rules (1) (Nakamura)
   
   Lecture Note 04   CafeOBJ Code 04  
5. [Dec.24 (Tue.)  09:20-10:50]  Inference with Rewriting Rules (2) (Nakamura)
   
   Lecture Note 05
6. [Jan.07 (Tue.)  09:20-10:50]  Constructor-based Inductive Theorem Prover (CITP) (2) (Gaina)
   
   Lecture Note 06  
7. [Jan.09 (Thur.) 11:00-12:30]  Formal Verification with CITP (Gaina)
   
   Lecture Note 07   tree.maude   th1.maude   th2.maude   th3.maude
8. [Jan.14 (Tue.)  09:20-10:50]  Proof Scores for Invariant Verification with State Patterns (Futatsugi)
   
   Lecture Note 08   qlock-sysProp.cafe   qlock-invPS.cafe   invDebug.txt   lec08-jaistRR.pdf  
   The CafeOBJ codes are supposed to be executed with the newest version of CafeOBJ (cafeobj-1.4.12p1).
9. [Jan.16 (Thur.) 11:00-12:30]  Proof Scores for Lockout Freedom Verification with Search Predicates (Futatsugi)
   
   Lecture Note 09   genCases.cafe   qlock-invPS-auto.cafe   boolFunEq.cafe   m-and-or.cafe   qlock-lofPS.cafe   lofDebug.txt   qlock-invPS-auto-2.cafe qlock-lofPS-2.cafe
   The CafeOBJ codes are supposed to be executed with the newest version of CafeOBJ (cafeobj-1.4.12p1).
10. [Jan.21 (Tue.)  09:20-10:50]  Model checking of trans-based system specifications (Ogata)
    
    Lecture Note 10   inv.cafe   inv.maude   mc_nonSec.cafe   mc_nonSec.maude   nspk.cafe   nspk.maude
11. [Jan.23 (Thur.) 11:00-12:30]  Theorem proving of trans-based system specifications (Ogata)
    
    Lecture Note 11   inv.cafe   nslpk.cafe   proof_isValid.cafe   proof_nonInCiph1.cafe   proof_nonInCiph2.cafe   proof_nonSec.cafe
12. [Jan.28 (Tue.)  09:20-10:50]  Analysis of trans-based system specifications with an integration of model checking and theorem proving (Ogata)
    
    Lecture Note 12  inv.cafe   inv.maude   mc_authInit.maude   mc_authInit2.maude   mc_ciphInConfirm.maude   mc_nonSec.maude   mc_randInConfirm.maude   nspk.cafe   nspk.maude   proof_authInit.cafe   proof_isValid.cafe
13. [Jan.30 (Thur.) 11:00-12:30]  Formal Verifying Dynamic Software Updating in CafeOBJ, a case study on RailCab System (Zhang)
    
    Lecture Note 13   inv.maude   lemma-1.maude   lemma-2.maude   lemma-3.maude   lemma-4.maude   lemma-5.maude   lemma-6.maude   lemma-7.maude   lemma-8.maude   railcab-citp-new.maude   railcab-trans-new.cafe   railcab-trans-new.maude   railcab-trans-old.cafe   railcab-trans-old.maude   railcab-trans-update-1.maude   railcab-trans-update-2.maude   railcab-trans-update.cafe
14. [Feb.04 (Tue.)  09:20-10:50]  Proof techniques for liveness and fairness (Preining)
    
    Lecture Note 14   qlock-freefair.cafe
    (For executing qlock-freefair.cafe you need qlock-sysProp.cafe   and qlock-invPS.cafe   from Lecture 8.)
15. [Feb.06 (Thur.) 11:00-12:30]  Examination
Only (paper) copies of the Lecture Notes 01,01a,...,14 (15 in total) can be brought into the examination.

---

Announcements

• [Dec.5 (Thur.), 2013] The home page of the course is ready.
• [Jan.17 (Fri.), 2014] Lecture Note 09 and qlock-lofPS.cafe are revised.
• [Jan.18 (Sat.), 2014] Two revised proof scores qlock-invPS-auto-2.cafe and qlock-lofPS-2.cafe are posted.

---

Assignments

• Assignment 1
  Annoucement: Dec.10(Tue) Deadline: Dec31.(Tue.)24：00
  • Assignment 1 (pdf file)
    
  • Template file for assignment 1 (text file with .cafe extension)
  • Numbers of the students whose answer emails for assignment1 are received (2014.1.1).
    
    The student who has sent answer email of assignment1 but can not find her/his number here should send e-mail to Futatsugi .
  Sample Answers are posted: Jan.1 (Wed.)
  • Sample answers to excercise 01
  • Sample answers to excercise 02
  
  
• Assignment 2
  Annoucement: Dec.24(Tue) Deadline: Jan.14(Tue)24：00
  • Assignment 2 (pdf file)
    
  • Numbers of the students whose answer emails for assignment2 are received (2014.1.15).
    
    The student who has sent answer email of assignment2 but can not find her/his number here should send e-mail to Nakamura and Futatsugi .
  Sample Answers are posted: Jan.15 (Wed.)
  • Sample answers to Assignment 2
  
  
• Assignment 3
  Annoucement: Jan.7 (Tue.) Deadline: Feb.5(Wed.)24:00
  (The office hour 13:30-15:00, Jan.7 (Tue.) is used for explaining this assignment; you also need to look into the CITP web page.)
  • Assignment 3 (text file)
    
  • pnat.maude (text file)
  • list.maude (text file)
  • cloud.maude (text file)
  • cloud.pdf (pdf file)

---

The students who have passed assignments and examination

Student numbers of the persons who got more than 59 out of 100 (20+20+25+35)

---

Installation of the CafeOBJ Language System

• Each attendee is expected to install CafeOBJ System version 1.4.11 to his/her own personal computer for executing examples and exercises of the lectures. The examples of the lectures are prepared for the version 1.4.11. You can obtain CafeOBJ binaries for Windows, MacOS and Linux from the following page:
  
  http://www.ldl.jaist.ac.jp/cafeobj/download.html
  
  
• The page explains how to install CafeOBJ on Windows, MacOS and Linux. Note that you may need to have the following three files in the "data" folder to install CafeOBJ on Windows 7:
  libeay32.dll
  ssleay32.dll
  vsinit.dll
  
  If so, please copy those three files in the "data" folder in the "cafeobj" folder before the installation.
  
  
• It is convenient to use an Emacs editor to interact with CafeOBJ. The editor allows you to execute a shell program, on which you can start CafeOBJ. You can use some editor functionalities (copy&paste, editing inputs to CafeOBJ, etc.) to interact with CafeOBJ. This is very convenient.
  In the JAIST information environment, just type 'mule' or 'emacs' if your PATH contains '/us/local/bin'.
  There are several implementations available on Windows:
  
  GNU Emacs on Windows
  Meadow
  

---

Reference Materials and Web Pages

• CafeOBJ official homepage
• Introduction to CafeOBJ System (by SEINO,Takahiro)： Primary concise introduction to CafeOBJ Language System

The followings are in Japanese.
• CafeOBJ入門(by 清野)：CafeOBJ言語システムの簡便な説明
• 日本ソフトウェア科学会のコンピュータソフトウェア誌に連載された『CafeOBJ入門』(全6回)
  CafeOBJ入門(1)-形式手法とCafeOBJ-
  CafeOBJ入門(2)-構文と意味-
  CafeOBJ入門(3)-等式推論と項書換システム-
  CafeOBJ入門(4)-証明譜による検証法-
  CafeOBJ入門(5)-認証プロトコルの検証-
  CafeOBJ入門(6)-通信プロトコルの検証-
  

---

http://www.jaist.ac.jp/~kokichi/class/i613-1312/
[ IS | JAIST ]