CP7010 CONCURRENCY MODELS - ANNA UNIVERSITY 1ST SEM CSE SYLLABUS REG-2013 - Anna University Internal marks 2018

CP7010 CONCURRENCY MODELS - ANNA UNIVERSITY 1ST SEM CSE SYLLABUS REG-2013

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