ANNA UNIVERSITY, CHENNAI
REGULATIONS - 2013
M.E. COMPUTER SCIENCE AND ENGINEERING
CP7010 CONCURRENCY MODELS
OBJECTIVES:
To model concurrency in FSP
To specify and check safety and liveness properties
To understand concurrency architectures and design
To apply linear temporal logic to safety and liveness analysis
To apply Petri nets for concurrency modeling and analysis
UNIT I FSP AND GRAPH MODELS
Concurrency and issues in concurrency – models of concurrency – graphical models – FSP &
LTSA – modeling processes with FSP – concurrency models with FSP – shared action – structure diagrams – issues with shared objects – modeling mutual exclusion – conditional synchronization – modeling semaphores – nested monitors – monitor invariants
UNIT II SAFETY AND LIVENESS PROPERTIES
Deadlocks – deadlock analysis in models – dining philosophers problem – safety properties –
single-lane bridge problem – liveness properties – liveness of the single-lane bridge – readers- writers problem – message passing – asynchronous message passing models – synchronous
message passing models – rendezvous
UNIT III CONCURRENCY ARCHITECTURES AND DESIGN
Modeling dynamic systems – modeling timed systems – concurrent architectures – Filter pipeline – Supervisor-worker model – announcer-listener model – model-based design – from requirements to models – from models to implementations – implementing concurrency in Java – program verification
UNIT IV LINEAR TEMPORAL LOGIC (LTL)
Syntax of LTL – semantics of LTL – practical LTL patterns – equivalences between LTL
statements – specification using LTL – LTL and FSP – Fluent proposition – Temporal propositions – Fluent Linear Temporal Logic (FLTL) – FLTL assertions in FSP – Database ring problem
UNIT V PETRI NETS
Introduction to Petri nets – examples – place-transition nets – graphical and linear algebraic
representations – concurrency & conflict – coverability graphs – decision procedures – liveness – colored Petri nets (CPN) – modeling & verification using CPN – non-hierarchical CPN – modeling protocols – hierarchical CPN – timed CPN – applications of Petri Nets
TOTAL : 45 PERIODS
OUTCOMES:
Upon Completion of the course, the students will be able to
Develop concurrency models and FSP
State safety and liveness properties in FSP
Verify properties using LTSA tool Explain concurrency architectures
Design concurrent Java programs from models
Apply Linear Temporal Logic to state safety and liveness properties
Assert LTL properties in FSP and check using LTSA tool Model and analyze concurrency using Petri nets
REFERENCES:
1. Jeff Magee & Jeff Kramer, “Concurrency: State Models and Java Programs”, Second Edition,John Wiley, 2006.
2. M. Huth & M. Ryan, “Logic in Computer Science – Modeling and Reasoning about Systems”,
Second Edition, Cambridge University Press, 2004.
3. B. Goetz, T. Peierls, J. Bloch, J. Bowbeer, D. Holmes, and D. Lea, “Java Concurrency in
Practice”, Addison-Wesley Professional, 2006.
4. Wolfgang Reisig, “Petri Nets: An Introduction”, Springer, 2011.
5. K. Jensen and L. M. Kristensen, “Colored Petri Nets: Modeling and Validation of Concurrent
Systems”, Springer, 2009.
6. Wolfgang Reisig, “Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case
Studies”, Springer, 2013.
No comments:
Post a Comment