 | Design and Processing of XML Languages |
| Course Descriptions |
 | UNU-IIST Home |
|
|
| |||||||
| Real-Time Systems: Specification, Verification, Refinement and Schedulability | |||||||||
Lecturer: Zhiming Liu
Duration of the Course: 25 hours, but a subset of contents can
be taught in 12 hours
Overview:
Fault-tolerance and timing have often been considered to be implementation issues of a program, quite distinct from the functional safety and liveness properties. Recent work has shown how these non-functional and functional properties can be verified in a similar way. However, the more practical question of determining whether a real-time program will meet its deadlines, i.e., showing that there is a feasible schedule, is usually done using scheduling theory, quite separately from the verification of other properties of the program. This makes it hard to use the results of scheduling analysis in the design, or redesign, of fault-tolerant and real-time programs. This course discusses how fault-tolerance, timing, and schedulability can be specified and verified using a single notation and model. This allows a unified view to be taken of the functional and nonfunctional properties of programs and a simple transformational method to be used to combine these properties. It also permits results from scheduling theory to be interpreted and used within a formal proof framework. The notation and model are illustrated using simple examples. Examples and exer cises will be given to relate this model to other well-known notations.
Aims and Objectives:
To provide with the course participants with main concepts, problems and techniq ues in the development of concurrent, distributed and real-time systems from both practical and theoreti cal perspectives; conceptual the understanding of the relationship between concurrency, distribution, real- time and fault-tolerance; fundamental understanding about the relationship between specification, verifica tion, refinement and scheduling analysis; basic ideas about the development and use of a formal metho d for the treatment of different problems.
Content:
-- Historical Background on Formal Methods: This is mainly to motivate Formal Techniques for Real-Time, Fault-Tolerance and Schedulability
-- An Informal Account on Real-Time systems
--- General Development process of a system
--- How develop a formal specification
-- Introduction to the Temporal Logic of Actions
-- Computational Model: Transition Systems
-- Formal Specification in TLA
-- Verification and Refinement in TLA
--- Fault-Tolerance as Refinement
--- Formal Treatment of Real-Time in TLA
-- Both Fault-Tolerance and Time
--- Relate Scheduling Analysis to Verification and Refinement
--- Fault-Tolerant Schedulability
--- Summing up
| Real-Time Systems: Specification, Verification, Refinement and Schedulability | |||||||||
|
|
| |||||||