Homework #1: Download the SPARK toolkit from http://libre.adacore.com. Work through the Tokeneer Discovery Tutorial at http://www.adacore.com/home/products/sparkpro/tokeneer/discovery/. Due: Monday, 14-Sep before class. (Nothing to hand in. Lecture will assume that you have gone through this tutorial.)
Please also review the last example in the webinar from today. You can download the webinar from http://www.adacore.com/inserts/webinars/, It is "Introducing SPARK Pro" (April 21). I will make several observations about that example in class on Monday and I will assume you are familiar with it.
Homework #2: (Due: Wednesday, 16-Sep) Download the archive of versions 0 through 2 of the Travel example from http://www.cse.msu.edu/~cse814/Public/F09/Homeworks/. It is the file “Travel0to2.tar.gz”. This is a gzipped tar file. Many archiving tools can unpack such archives. For instance, I have PowerArchiver 2001, and it unpacks it fine. Or you can unpack it manually by downloading it to one of the CSE severs, ssh to the server, type “gzip Travel0to2.tar.gz” and then “tar xvf Travel0to2.tar”. This should extract it to a directory called “Travel0to2”.
This directory has three projects in it. The project files are the files with the
extension “.gpr”. Double-clicking on any
of these three files should bring up the corresponding project in GPS. I went over versions 0 and 1 in class today.
Spend some time before class on Wednesday to understand these
examples---especially version 2. You
should build the project and execute it.
Then scroll through the files in the project and try to understand what
each package comprises and what each procedure and function is doing. You can look up information about
Come to class with any questions you have about the example. After answering your questions about it, I will proceed to use it to explain the annotations needed for information flow analysis. You will get a lot more from the explanation if you understand the example.
Homework #3: Due Monday 28-Sep. Download “travel03.tar.gz” from the homework directory (http://www.cse.msu.edu/~cse814/Public/F09/Homeworks/). Unpack it and follow the instructions in the README.TXT file.
Homework #4: Due Monday 26-Oct. See here.
Homework #5: (Due Monday 16-Nov).
Problem 1: Exercise A.1.6 on page 233 of the Alloy book (Software Abstractions, D. Jackson). Use directed graphs and trees for this exercise (a warm up for more interesting things).
Problem 2: Download the files hotel_locking_ops_hw.als, hotel_locking_hw.als. and hotel_locking.thm. The Alloy files (.als files) are from Figs. 6.10 and 6.11 on pages 198 and 199 of the Alloy book, with some minor name changes. The former defines the operations, but does not include the trace specifications. The last file (.thm file) is a theme file to use when viewing instances.
Execute the command in the first of the Alloy files (hotel_locking_ops_hw.als). View the instance that is generated using the default settings. Then load the theme from within the instance window (in the Theme menu, select “load theme”). Generate several different instances by pressing “Next” several times.
Next, write four commands to use in sanity testing this specification: 1) a command that generates a Checkin event, 2) a command that generates a Checkout event, 3) a command that generates an Entry event, 4) a command that generates sequences consisting of one of each type of event and simulating different orders in which the specification permits them to occur. Do not use the trace idiom for this exercise. Instead, define predicates that constrain the pre and post times of the events to model the fact that they occur in sequence.
Now open the second Alloy file (hotel_locking_hw.als). Run the command to check NoBadEntry. It should produce a counter model. Load the theme file and study the counter model. Be sure you believe the trace satisfies the specification and that you understand how the guest managed to enter the room even though the room was owned by another guest.
The predicate NoIntervening is just the fact NoIntervening on page 200 written as a predicate. Checking the assertion GuardedNoBadEntry should be equivalent to asserting NoIntervening as a fact and then checking NoBadEntry, as described on page 200. Thus, you would expect that checking GuardedNoBadEntry will not produce any counter models. Run the GuardedNoBadEntry check and verify that this is in fact the case.
But GuardedNoBadEntry is not actually valid. The specification of one of the operations is not strong enough to prevent “bad” entries. The Alloy analyzer did not find any counter model because no counter model exists within the given scope.
Use the analyzer to “debug” the specification. Increase the scope until you find a counter model. Study the counter model to identify the operation that is not behaving “as expected”. Fix the operation and then verify that now no counter models to GuardedNoBadEntry exist within the larger scope.
Problem 3: View a phone system as a collection of endpoints and a centralized database that maintains information about which endpoints are connected to each other. Model the structure of this database, along with the operations that modify it when a conference call is established, when endpoints are added and dropped, etc. Simulate some interesting scenarios, and formulate and check some assertions. Write up a short description of your model, what the scenarios illustrate and what your assertions show. (This is the “open-ended” case study (c) of p. 251.)
You will hand in five files for this assignment:
1) spanning.als – the solution to problem 1;
2) hotel_ops_hw.als – from problem 2;
3) hotel_hw.als – from problem 2;
4) conference_calling.als – your solution for problem 3;
5) your write up for problem 3
Homework #6: (Due Wednesday 2-Dec)
This homework will be worth 8 points. To earn these 8 points, you need only do problems 1 & 2. You can earn an additional 8 points, if you need some extra credit, by also doing problems 3 and 4. Hand in the assignment by emailing me a single FSP file with your solutions to problems 2-4 and either a pdf or a plain text file containing the traces and explanations requested.
Problem 1: Load the thread_demo example (File=>Examples=>chapter3=>thread_demo). Compose the THREAD_DEMO process. Run an animation to generate a trace of your choosing (minimum length of 6). Indicate the trace you generated and the states of the three LTSs at the start and after each event in the trace. For each state of the ||THREAD_DEMO LTS, indicate the pair of states of the a:ROTATOR and b:ROTATOR processes represented. (You might want to set "Options=>Multiple LTS in Draw window" and position the three LTSs so that you can see all three as you run the trace.)
In general, composing several LTSs produces an LTS whose states are essentially the product of the states of the component LTSs. Thus, in the THREAD_DEMO example, you might expect the composed LTS to have 9 states. Explain why it has only 5 states. What are some state pairs of the a:ROTATOR and b:ROTATOR LTSs that have no counterpart in the THREAD_DEMO automaton?
Note on Problems 2-4: Your book has a model of the classic dining philosophers problem. The variation I am giving you is simpler to model because there is no distinction between the forks. I recommend that you do these problems after reading chapter 4 carefully and without first reading the dining philosophers model in the later chapters so that you are not accidentally biased to make the models more complex than they need to be. I will be looking for simplicity in your models. (The whole point of modeling is to abstract a complex system to a level appropriate for some analysis.)
Problem 2: For this problem, you will create an FSP model for a variation of the classic dining philosopher problem. In this variation, the forks are kept in a drawer. A philosopher spends her life thinking and eating. Before eating, she retrieves any two forks from the drawer. After eating and before returning to thinking, she returns the forks to the drawer (after washing them, of course J ---but this detail can be left out of the model since it does not affect synchronization). The drawer holds a maximum of 5 forks and there are 5 philosophers.
For this first model, assume that the philosopher retrieves the two forks from the drawer atomically. Run some animations and provide a trace that you generated showing that, unlike in the classic dining philosopher problem, your model allows "adjacent" philosophers to eat at the same time as long as no other philosophers are also eating.
Use the LTSA safety check to verify that deadlock cannot occur.
Problem 3: For this problem, you are to create a model for the same variation of the dining philosophers problem, but in this model, assume that a philosopher first retrieves a fork for her left hand and then a fork for her right hand (as two atomic actions). Use the LTSA safety check to determine if deadlock can occur. Give a trace to the deadlock, if so. Otherwise, explain how your model prevents deadlock.
Problem 4: Add a "test" process to your model in problem 3 to check that no more than two philosophers can ever be simultaneously holding their right forks.
Paper presentation title:(Due Friday 20-Nov)
I need to receive an email from you with the title for your presentation by the end of day Friday so I can schedule the talks. Please indicate your preference for presentation day, the paper author(s) and a title. (Several of you have already done this. If you received a reply from me that I received the information, you do not need to resend. Although, if you did not indicate a preference for presentation day, you may want to.) All presentations will take place on Monday Dec 7 or Wednesday Dec 9 during the normal class time (3:00 - 4:20 pm) or Monday Dec 14 in the time scheduled for our final exam (3:00 - 5:00 pm). I will try to accommodate preferences for specific days, if possible, but I may not be able to.
You can find a presentation about giving research presentations here. I will evaluate your presentation according to the guidelines in this presentation.
I expect to post a schedule of talks early next week (Nov 23 or 24).
|
7-Dec (Monday) |
|
|
9-Dec (Wednesday) |
|
|
14-Dec (Monday) |
|
Term paper/project: (Due Wednesday 9-Dec)
Your term project or term paper needs to investigate a topic related to formal methods or their use. It should cover a topic not covered in class or treat a topic that we covered in more depth. The project write-up/ term paper should demonstrate your ability to synthesize information from different sources and draw (and support!) reasoned conclusions. A part of the grade will be based on clarity, good organization, and correct use of English.
You must comply with ACM policy and procedures with respect to plagiarism:
http://www.acm.org/publications/policies/plagiarism_policy.
You should submit your paper electronically in PDF format and follow ACM's proceedings format strictly, including font sizes, line spacing, and margins:
http://www.acm.org/sigs/publications/proceedings-templates
Your paper should be on the order of 6 - 8 pages (excluding references). Please speak to me if you feel you need to go much beyond that. Your paper must, of course, cite references (but the page count does not include references, so they might increase your page count by an extra page).