til NTNUs webside to Department of Telematics to Faculty of Electrical Engineering and Telecommunications

COURSE TM 8103:  FORMAL METHODS.

 

 

 

A: General

 

Course responsible: Professor Finn Arve Aagesen, ITEM

 

Content: Focus is on theory on validation/verification of communication systems functionality. The theory covers

state machine based validation  in non-reduced state space, Process algebra, Rewriting logic and reasoning based

on  UML constraints. A submission of compulsory group assignment, which based on model validation tool PROMELA  and SPIN
http://spinroot.com/spin/Man/Quick.htmlwhich is handled in the book: G.J. Holzmann:  SPIN Model Checker, The: Primer and Reference Manual is compulsory.

.

Background: Knowledge to Finite and Extended State Machine is a prerequisite.

Form: Lectures, self study and colloquiums.

Learning goals: To be able to validate the correctness properties of a  functional model and

also to verify the consistency  between models related to the various phases of functionality life cycle,

as the consistency between required properties and functional design and the consistency between

functional design and implementation design.

 

 

Lecturers:  Vladimir Oleshchuk, Cyril Carrez, Mazen Malek, Chutiporn Anutariya

Examination: 1/6-04, Oral

 

B: Contents, lectured load equivalents and method:

 

General papers:                        4 hours,            Self study

Promela and Spin                     12 hours,          Self study, lectures, colloquiums and assignment

Process Algebra:                      10 hours,          Self study, lectures and colloquium

Rewriting logic and Maude:       6 hours,            Lectures

UML constraints                       6 hours,            Lectures

                                                -----------

Totally                                      38 hours

 

C: Syllabus (Draft)

 

General papers:

E. Brinksma:  What is the Method of Formal Methods, FORTE 91,

Sydney November 1991.

B. Pehrson:    Protocol Verification for OSI, Computer Systems and

ISDN Systems no 18, 1989-1990.

 

Spin and Promela:

G.J. Holzmann:  SPIN Model Checker, The: Primer and Reference Manual

ISBN: 0-321-22862-6, Publisher: Addison Wesley Professional, 2004

http://www.aw-bc.com/catalog/academic/product/0,4096,0321228626-PRE,00.html

 

Introduction:     Ch. 1 - 5 pp.1-126                   (126pp)
Foundation:      Ch. 6-9 pp. 127-216                (90pp)
Practice:           Ch. 11,12,14,15                       (102pp)

Total  Holzmann:     318pages

 

Process Algebra:

R. Milner: Communication and Concurrency,

Prentice Hall 1989, ISBN 0-13-115007-3 PBK.

 

Ch.1- Ch.4: s.11 - s. 101                                 (90pp)

Ch.5.1-Ch.5.3 and Ch. 5.6: s. 106-113, 

s. 123-128                                                       (14pp)

Ch.7 :s.150-s.169                                            (10pp)

Total Milner:     114pages                                            

                                

Rewriting Logic and Maude:

Narciso Martí-Oliet and José Meseguer, "Rewriting logic as a logical and

semantic framework", RWLW96, First International Workshop on Rewriting

Logic and its Applications, Asilomar Conference Center, Pacific Grove, CA, USA, September 3-6, 1996,

http://www1.elsevier.com/gej-ng/31/29/23/29/23/63/tcs4012.ps

 

 Mark-Oliver Stehr and Carolyn Talcott, Plan in Maude: Specifying an Active Network Programming Language,

In 4th International Workshop on Rewriting Logic and its Applications,

(WRLA'02), http://maude.cs.uiuc.edu/papers/postscript/stehr-talcott-02wrla.ps.gz

 

 Maude 2.0 Manuel, The Maude homepage: http://maude.cs.uiuc.edu

 http://maude.cs.uiuc.edu/manual/maude-manual.pdf

 

UML constraints

 

References:

[1] Jos B. Warmer and Anneke G. Kleppe: The Object Constraint Language:

Precise Modeling with UML (1999)

[2] OMG: UML Object Constraing Language Specification (2003)

http://www.omg.org/docs/ad/03-01-07.pdf

  

Contents:

  - Introduction

  - OCL Language Description

  - Abstract and Concrete Syntax

  - Semantics described using UML

  - The Use of OCL Expressions in UML Models

  - Interchange Format

 

D. Logistics:

 

30/1:    13.15-14.00: General overview

30/1:    14.15-15.00: Planning on the logistics for

colloquiums for the stuff from Holzmann and Millner

in February and March. (Vladimir)

 

13/2:    8.30-12.00       Holzmann.        (Colloquium and Lecture, Vladimir, Read Ch.1-5 in beforehand)
5/3:      8.30-12.00       Holzmann         (Colloquium Vladimir)

2/4:      8.30-12.00       Millner              (Colloquium Vladimir)
16/4:    8.30-12.00       Millner              (Colloquium Vladimir)

 

23/4:    9.15- 12.00      Rewriting Logic and Maude (Lecture Mazen/Cyril)

30/4:    9.15 -12.00      Rewriting Logic and Maude (Lecture Mazen/Cyril)

 

6/5:      9.15-12.00:      UML Constraints (Lecture Chutiporn Anutariya)

7/5:      9.15-12.00       UML  Constraints (Lecture Chutiporn Anutariya )

 

                                   

NTH March 3, 2004

 

Finn Arve Aagesen

Course Responsible