<< >> ^

SFT4020

Specifying non-sequential and real-time systems

A Sajeev and B Durnota

6 points
* 4 hours per week
* Second semester
* Caulfield

Objectives At the completion of this subject students should know the specification characteristics of non-sequential and real-time systems; know the proving properties of non-sequential systems at an introductory level; and be able to develop specifications of non-sequential and real-time systems using different approaches.

Synopsis The basic issues and characteristics of non-traditional systems: concurrent, distributed, parallel, reactive, real-time and trusted systems. Some approaches to specifying these systems: statecharts, Petri nets, process calculi and temporal logic. Use of model-based specification. Relations between the various approaches. Proving properties of non-sequential and real-time systems. Case studies in specifying non-sequential systems.

Assessment Assignments: 100%

Recommended texts

Chandy K M and Misra J Parallel program design: A foundation Addison-Wesley, 1988

Diller A Z: An introduction to formal methods 2nd edn, Wiley, 1994

Fencott C Formal methods for concurrency Chapman and Hall, 1994

Levi S-T and Agrawala A real-time system design McGraw-Hill, 1990

Manna Z and Pnueli A The temporal logic of reactive and concurrent systems. Specification Springer-Verlag, 1992

Milner R Communication and concurrency Prentice-Hall, 1989

Peterson J L Petri net theory and the modeling of systems Prentice-Hall, 1981


<< >> ^
Handbook Contents | Faculty Handbooks | Monash University
Published by Monash University, Clayton, Victoria 3168
Copyright © Monash University 1996 - All Rights Reserved - Caution
Authorised by the Academic Registrar December 1996