|
The
Real-Time Process Algebra (RTPA)
¤ SENG
523 Lecture Notes
·
Lecture 1 [PPT] [PDF]
·
Lecture 2 [PPT] [PDF]
·
Lecture 3 [PPT] [PDF]
·
Lecture 4 [PPT] [PDF]
·
Lecture 5 [PPT] [PDF]
·
Lecture 6 [PPT] [PDF]
[TSS Model-PDF] [TSS
Model-MSW] [TSS
Design]
·
Lecture 7 [PPT] [PDF]
·
Lecture 8 [PPT] [PDF]
·
Lecture 9 [PPT] [PDF]
·
Lecture 10 [PPT] [PDF]
·
Lecture 11 [PPT] [PDF]
·
Lecture 12 [PPT] [PDF]
·
Lab 1 [PPT]
[Reference
Architecture]
·
Lab 2 [PPT]
[Reference
Model]
·
Lab 3 [PPT]
·
Tutorial 1 [RTPA]
[Big-R]
· Tutorial 2 [RTPA-Deductive
Semantics] [RTPA-Operational
Semantics] [RTPA-Denotational
Semantics]
· Tutorial 3 The Framework Model of ATM: [PDF]
[MSW]
¤ RTPA
notations and system modeling methods
· The RTPA
notations
[MSW |
PDF]
·
The RTPA
scheme for system specification and refinement [PDF]
¤ Case
Studies on RTPA specifications
·
RTPA Case studies A: ADT1 - A Stack
[PDF]
·
RTPA Case studies B: ADT2 - An Array
(n-D)
[PDF]
·
RTPA Case studies C: A Telephone Switching System (TSS)
[MSW |
PDF |
Paper]
·
RTPA Case studies D: A Lift Dispatching System (LDS)
[MSW |
PDF | Paper]
· RTPA Case studies E: An ATM System (ATM)
[MSW | PDF]
[Ref. Model in RTPA]
¤ Related
Formal Methods
·
CSP
·
Z
[Reference
Manual]
·
Object-Z
·
B
·
SDL
¤ Related
Courses
·
LINKS
|