ECE658: Course Readings | |||||||
| |||||||
Required textbooks:
|
Logic in computer science: modelling and reasoning about systems Michael R. A. Huth, Mark Ryan, Cambridge University Press, 2000. |
 |
|---|---|
|
The Temporal Logic of Reactive and Concurrent Systems (Specification) Zohar Manna, Amir Pnueli, Springer-Verlag, 1992.
|
 |
|
Communicating Sequential Processes C. A. R. Hoare. Prentice Hall, 1985
http://www.usingcsp.com/cspbook.pdf
|
 |
Papers to be covered:
Actors: A Unifying Model for Parallel and Distributed Computing.
G. Agha and W. Kim.
Journal of Systems Architecture, 1998,
EuroMicro Society/Elsevier, Vol.45, pp. 1263-1277, 1999.
Modeling and Verification of Reactive Systems using Rebeca,
Sirjani M., Movaghar A, Shali A., and de Boer F. S.,
Fundamenta Informaticae, Dec. 2004
Reo: A Channel-based Coordination Model for Component Composition,
F. Arbab,
Mathematical Structures in Computer Science, Vol. 14, No. 3, pp. 329-366, June 2004.
Modeling Component Connectors in Reo by Constraint Automata,
F. Arbab, C. Baier, J.J.M.M. Rutten and M. Sirjani,
Proceedings of FOCLASA'03, Marseille, France, September 2003, Electrical Notes in Theoretical Computer Science, Elsevier Science.
Further reading:
Concurrency
[1] Elements of Interaction (1992 Turing Lecture), Milner R., Comm. of the ACM, Vol. 36, No. 1, 1993, PP. 78-89.
Formal verification, model checking, temporal logic:
[2] Automating modular verification, Alur R., de Alfaro L., Henzinger T. A., and Mang F. Y. C., CONCUR: 10th International Conference on Concurrency Theory, Lecture Notes in Computer Science, Springer-Verlag, Berlin, Germany, 1999, pp. 82--97.
[3] Computer Aided Verification, Alur R., Henzinger T. A., 1999.
[4] Model checking, Clarke E. M., Grumberg O., and Peled D. A., The MIT Press, Cambridge, Massachusetts, 1999.
I/O Automata
[6] Distributed algorithms, Lynch N. A., Morgan Kaufmann, San Francisco, CS, 1996.
CCS and Pi-Calculus
[7] A Calculus on Communicating Systems, Milner R., Lecture Notes in Computer Science, vol. 92, Springer-Verlag, Berlin, Germany, 1980.
Actors and Rebeca
[9] Actors: A model of concurrent computation in distributed systems, Agha G., MIT Press, Cambridge, MA, USA, 1990.
[10] The Structure and Semantics of Actor Languages, Agha G., Foundations of Object-Oriented Languages: REX School workshop, LNCS 489, 1991, PP. 1-59.
[11] Modelling Concurrent System:Actor, Nets, and Problem of Abstraction and Composition, Agha G., Applications and Theory of Petri Nets, Lecture Notes in computer Science, Vol. 1091, Springer-verlag, 1996.
[12] A front-end tool for automated abstraction and modular verification of actor-based models, Sirjani M., Shali A, Jaghoori M., Iravanchi H., and Movaghar A., Proceedings of ACSD 2004, Hamilton, Canada, pp. 145-148, IEEE Computer Society, June 2004.
Coordination Languages
[13] Abstract Behavior Types: A Foundation Model for Components and Their Composition, Arbab F., LNCS, Springer-Verlag, Vol. 2852, pp. 33-70, September 2003.
[14] A Coinductive Calculus of Component Connectors , Arbab F., Rutten J., LNCS, Springer-Verlag, Vol. 2755, pp. 35-56, November 2003.
[15] Coordination Models and Languages, Arbab F., Papadopoulos G., Advances in Computers, Vol. 46, Academic Press, 1998.
[16] What Do You Mean, Coordination?, Arbab F., in the March '98 Issue of the Bulletin of the Dutch Association for Theoretical Computer Science (NVTI).
[17] Models and Temporal Logics for Timed Component Connectors, Arbab F., Baier C., de Boer F.S., Rutten J., International Journal on Software and Systems Modeling, Springer, to appear in 2005.
Tools
[18] NuSMV user manual
http://nusmv.irst.itc.it/NuSMV/userman/index-v2.html
http://khorshid.ut.ac.ir/~rebeca
http://spinroot.com/spin/Man/Manual.html
Reo
[21] Effective Modeling of Software Architectural Assemblies Using Constraint Automata, N.R. Mehta, M. Sirjani, F. Arbab.
[22] Reo: A Channel-based Coordination Model for Component Composition, F. Arbab, Mathematical Structures in Computer Science, Vol. 14, No. 3, pp. 329-366, June 2004.