CP7010 CONCURRENCY MODELS - ANNA UNIVERSITY 1ND 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.

URL: http://feedproxy.google.com/~r/StudentsBlog100/~3/3rm_GiGZqVI/cp7010-concurrency-models-anna-univ-pg-cse-2nd-sem-syllabus.html