The Hitachi Lectures:
A Rôle of Formal Methods in Modelling Application Domains
7-8 August 2003
Ohzenji, Asao-ku, Kawasaki, Japan

Dines Bjørner
CSE: Computer Science and Engineering
IMM: Informatics and Mathematical Modelling
Building 322, Richard Petersens Plads
DTU: Technical University of Denmark
DK-2800 Kgs.Lyngby, Denmark
E-Mail: db@imm.dtu.dk, URL: www.imm.dtu.dk/~db

July 29, 2003: 4:15 pm

Contents

• Abstract
• Administrative Information
• Lecture Plan
• RAISE: Rigorous Approach to Industrial Software Engineering
• About this document ...

Abstract

After a brief introduction to some standard discrete mathematics notation and to CSP (Communicationg Sequential Processes) I cover five application areas for medium-to-large scale software systems:

• Documents (rather superficially),
• E-Commerce,
• Production Planning, Monitoring and Control,
• Railways, and
• Freight Logistics.

The aims of the lectures is to show how one can conquer the seeming complexity of their underlying domains, while the objectives of the lectures is to suggest that proper, professional software development ought be based on the use of formal specifications, from domains, via requirements, to software design.

Administrative Information

• This document presents the lecture plan for two days of lectures at the Systems Development Laboratory
  Hitachi, Ltd., 1099 Ohzenji, Asao-ku, Kawasaki 215-0013, JAPAN.
• Thursday 7 and Friday 8 of August, 2003, 10 am - 4 pm.
• Host Mr. Hidetaka Kondoh, kondoh@sdl.hitachi.co.jp
  Voice: +81-44-966-9111 (Ext. 3022), Fax: +81-44-959-085.
• Documents marked *** below constitute (``formula only'') slides for the lectures.
  As noted, they are ``backed up'' by detailed papers, reports and notes.
• You are invited to inspect:
  • The SE Book
    Provides documents for Graduate Course in Formal Aspects of SE
  • An Introductory Course in SE
    Provides documents for an informal Undergraduate Course in SE

Lecture Plan

1. Thursday morning, 7 August
   • *** Opening First Discussion of Formal Methods in European Industry
   • *** The Notation to be Used (RSL)
   • *** Example 1: (First part) A Document System
2. Thursday afternoon, 7 August
   • *** Example 1: (Second Part) A Document System
   • *** Example 2: An E-Commerce System This lecture is supported by the following paper being published:
     • Domain Models of ``The Market'' -- in Preparation for E-Commerce
     Ongoing Discussion of Formal Methods in European Industry
3. Friday morning, 8 August
   • *** Example 3: A Project Management System This lecture is supported by the following internal report:
     • PIMaCS: A Project Planning, Information, Monitoring, Control and Communication System
   • *** Example 3: (First part) A Railway Domain Model This lecture is supported and extended by the following published papers:
     • Formal Software Techniques in Railway Systems
     • Computing Systems for Railways: A Rôle for Domain Engineering
4. Friday afternoon, 8 August
   • *** Example 3: (Second Part) A Railway Domain Model This lecture is extended by the following published papers:
     • Dynamics of Railway Systems:
       • Extended Paper Version
       • Talk Slide Version
     • Train Maintenance Routing
     • Railway Staff Rostering
   • *** Example 4: A Logistics System This lecture is supported by the following internal note:
     • Logistics, a rather incomplete Note
   • *** Closing Last Discussion of Formal Methods in European Industry

All lecture slides are assembled in one document: Four slides to a page. 

RAISE: Rigorous Approach to Industrial Software Engineering

• The course will exemplify RAISE
• We kindly refer you to: RAISE
• We kindly refer you to: The Formal Methods Home Page
• We kindly refer you to: The CoLogNET Formal Methods Home Page

...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...

/home/db/tokyo/lectures.tex

About this document ...

The Hitachi Lectures:
A Rôle of Formal Methods in Modelling Application Domains
7-8 August 2003
Ohzenji, Asao-ku, Kawasaki, Japan

This document was generated using the LaTeX2HTML translator Version 2K.1beta (1.47)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html -split 0 -toc_depth 6 lectures

The translation was initiated by on 2003-07-29