课程主页
上课时间地点
每周三7-8节
理教116
答疑时间地点
每周二、周三晚6:00 - 8:00
理科楼1484

主要阅读材料
1. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.
2. Gerald Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2004. (北大图书馆)
可选报告论文
1. Farhad Arbab, Christel Baier, Frank de Boer and Jan Rutten. Models and Temporal Logical Specifications for Timed Component Connectors. In International Journal on Software and System Modeling. vol. 6(1), pages 59-82, 2007.
2. Sascha Kluppelholz and Christel Baier. Symbolic Model Checking for Channel-based Component Connectors. In Science of Computer Programming. vol. 74(9), pages 688-701, 2009.
3. Kai Lampka, Markus Siegle, Joern Ossowski and Christel Baier. Partially-shared zero suppressed multi-terminal BDDs: concept, algorithms and applications. In Formal Methods in System Design. vol. 36, pages 198-222, 2010.
4. John Derrick and Heike Wehrheim. On using data abstractions for model checking refinements. In Acta Informatica. vol. 44, pages 41-71, 2007.
5. More articles will be added to the list later.
其它阅读材料
1. Doron Peled, Software Reliability Methods, Springer, 2001. (数学学院图书馆已订购)
2. Edmund Clarke, Orna Grumberg and Doron Peled. Model Checking. MIT Press, 1999. (数学学院图书馆)
3. Farhad Arbab. Reo: A Channel-based Coordination Model for Component Composition. In Mathematical Structures in Computer Science, Cambridge University Press, Vol. 14, Issue 3, pages 329-366, 2004.
4. Sun Meng,Farhad Arbab, Bernhard K. Aichernig, Lacramioara Astefanoaei, Frank S. de Boer and Jan Rutten. Connectors as Designs: Modeling, Refinement and Test Case Generation. Accepted by Science of Computer Programming.(contact Sun Meng for copy of this paper).
5. Sun Meng and Farhad Arbab. QoS-Driven Service Selection and Composition Using Quantitative Constraint Automata. In Fundamenta Informaticae, Vol. 95(1), pages 103–128, 2009.
6. Christel Baier, Tobias Blechmann, Joachim Klein and Sascha Kluppelholz. A Uniform Framework for Modeling and Verifying Components and Connectors. In Proceedings of Coordination 2009, LNCS 5521, pages 247-267, Springer, 2009.
7. Christel Baier, Marjan Sirjani, Farhad Arbab and Jan Rutten. Modeling Component Connectors in Reo by Constraint Automata. In Science of Computer Programming, Vol. 61, pages 75-113, 2006.
8. Farhad Arbab and Jan Rutten. A Coinductive Calculus of Component Connectors. In Recent Trends in Algebraic Development Techniques. LNCS 2755, pages 34-55, Springer, 2003.
9. Ramtin Khosravi, Marjan Sirjani, Nesa Asoudeh, Shaghayegh Sahebi and Hamed Iravanchi. Modeling and Analysis of Reo Connectors Using Alloy. In Coordination'08, LNCS 5052, pages 169-183, Springer, 2008.
10. Natallia Kokash, Christian Krause and Erik de Vink. Data-Aware Design and Verification of Service Compositions with Reo and mCRL2. In Proceedings of SAC'10, ACM, 2010.
11. Natallia Kokash, Christian Krause and Erik de Vink. Reo + mCRL2: A Framework for Model-Checking Dataflow in Service Compositions. submitted to Formal Aspects of Computing. 2011.
12. More articles will be added later.