Training Reading List for New Comers
This reading list is to equip new MS students with the basic knowledge required to conduct research in the SWTVlab. This seminars starts from April and ends in early June, just before the final exam.
Each part of seminars consists of one main paper and one case study paper. You have to download and try a corresponding tool with various examples. Also, you have two assignments for each part; one is easy and the other is a little bit harder.
For rewriting assignments, a key point is to get a concrete understanding of the syntax of a corresponding language and to understand a model and requirements accurately. Therefore, do not rewrite a model blindly character by character, but pay careful attention to understand what you are typing.
Part I: Process Algebra Basics (2 weeks)
- Process Algebra by R.Cleaveland and S.Smolka (up to sect. 2)
- End-to-End Deployment of Formal Methodology by M.Kim and I.Kang.
- Concurrent Workbench of New Century homepage (cwb-nc.zip)
- Assignments:
- Manually rewrite the example of "End-to-End ..." and check that you have the same result from CWBNC tool.
- Redesign a system model of the example as you want. Then, prove that your model satisfies the requirement properties.
Part II: Model Checking Basics (2 weeks)
- The Model Checker SPIN by G.Holzmann, IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, VOL. 23, NO. 5, MAY 1997
- Formal Analysis of a Space Craft Controller using SPIN by K.Havelund, etc.
- Spin home page
- Assignments:
- Manually rewrite leader and leader2 examples in the spin's example directory and check that you have the same result from Spin
- Redesign a multiple reader/writer system model in Promela. Then, prove that your model satisfies the requirement properties.
Part III: Runtime Verification (2 weeks)
- Java-MaC: A Run-Time Assurance Approach for Java Programs by M.Kim, etc.
- Verisim: Formal Analysis of Network Simulations by K.Bhargavan, etc
- Java-MaC home page
- Assignments:
- Manually rewrite PEDL and MEDL scripts in the MAV example (an example in the MaCSware 0.90) and instrument the MAV program to check that you get an expected result from the Runtime Checker.
- Instrument and check the multiple RW system described in Section 3.3.3.1 "Readers and Writers" of "Concurrent Programming in Java: Design Principles and Pattern" (2nd ed by Doug Lea). You should check requirement properties described in "End-to-End ..." by writing down corresponding PEDL and MEDL scripts for the requirements.
NOTE: Install a full package of Cygwin on your windows machine for your future convenience.
