CP7010 CONCURRENCY MODELS Syllabus - Anna University ME CSE 2nd Semester Regulation 2013 CP7010 Syllabus
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
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.
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
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.