CIS*6650*03
Formal System Modeling with CSP [0.50]

Course Outline for Winter 2004

INSTRUCTOR

COURSE LINKS

Bill Gardner

 

 

Class Schedule

office

Reynolds 105

 

 

 

phone

824-4120 x52696

Resources

 

 

e-mail

wgardner@cis.uoguelph.ca

 

 

 

web

www.cis.uoguelph.ca/~wgardner

 

 

 

NOTE: This is a graduate reading course in the CIS department with strictly limited enrolment. The Instructor's signature is required to register for this course.

Reading course description

In-depth study of formal process algebra CSP (Communicating Sequential Processes), and use in modeling computer systems. Use of software tools for simulation and formal verification of CSP specifications. Techniques for system synthesis from CSP specifications.

Prerequisites

CIS*6090 is recommended, or similar background in embedded systems. Any background in formal methods will be helpful.

Co-examiner: T. Wilson

Overview

The immediate objective is to prepare students for research in system synthesis (i.e., automatic source code generation) from formal specifications using CSP. To do this well, it is necessary to learn the constructs of the CSP process algebra, and become familiar with using those constructs to model concurrent systems. Another objective is to recognize what properties of concurrent systems can be formally verified (e.g., absence of deadlock), and learn how to use verification tools to check them. Still another objective is to develop CSP case studies for use in system synthesis research. The goal is to achieve software and hardware synthesis for embedded systems from CSP specifications. Knowledge and use of formal methods are uncommon in Canadian industry, and it is hoped that this training of "high-quality personnel" will help to widen that use where it is most beneficial.

Organization of course work

There will be a 2-hour seminar-like study session each week based on the textbook, with each participant taking turns leading the presentation and discussion. During the week we will be working chapter problems and preparing to discuss the solutions at the next study session.

Separately, students will be working through tutorials and carrying out labs on the Probe and FDR tools, which will be employed in conjunction with textbook problems.

Students will carry out a literature survey of current research (focus is negotiable). At the end of the course, students will give a presentation on their survey results and hand in a written report.

Course topics

  • The CSP language, by means of studying a textbook, concentrating more on practical use and less on theoretical foundations
  • The use of Probe (simulation) and FDR (verification) software tools, from Formal Systems (Europe) Ltd.
  • The various proposals for introducing the notion of time to CSP, which was not part of the original process algebra, but is important for modeling real-time systems
  • The state of current research in (a) system modeling with CSP, and (b) system synthesis from CSP or other formal methods

    • Textbooks

    Required text

    Concurrent and Real-time Systems: The CSP Approach, by Steve Schneider, Wiley, 2000.

    Recommended texts

    The Theory and Practice of Concurrency, by A.W. Roscoe, Prentice Hall, 1998.

    Determination of final grade

    Study sessions (participation and leading)

    20%

    Labs (creating and doing labs with Probe and FDR)

    20%

    Case study (creating CSP case study and implementing with CSP++)

    25%

    Literature review and written report

    25%

    Presentation of literature review

    10%

    According to CIS policy on reading courses, students are responsible for submitting monthly progress reports to the co-examiner. Failure to submit these reports in a timely manner will impact the final grade.