CSci 420/520: Homework 11

Cleanroom Black Box Specification

Due Monday, November 28th by 1pm.

Summary

BlackBoxGUI is a software tool for creating and analyzing black box specifications. It allows you to define stimulus histories in a formal manner, then analyze your overall specification for consistency and completeness. In this assignment you will use the tool to specify the external behavior of a web browser.

Make sure you have BlackBoxGUI running as described in the tools setup document. If you want to run the program locally, you can get it from ~coppit/software/black-box/BlackBoxGUI.jar. You will need Java 5 to run it.

Writing Histories

The BlackBoxGUI tool provides a language for writing histories that is similar in spirit to LTL. For example, one can specify any history in which B follows A as any:A:any:B:any. The language is more flexible, however, in that it supports a count operator to count the number of stimuli, as well as simple arithmetic.

For an overview of the language, select "How to write histories" from the help menu. For examples, of the use of each type of syntax element, select "Look up a syntax element" from the help menu.

The author of the tool has recently added a response operator to the language. It will match any sequence of stimuli that result in the specified response. For example, any:response Print will match any history that produces the response Print for its final stimulus.

WARNING: There was a bug in the parsing of arithmetic expressions in the tool before Nov 21. If you downloaded your own copy of BlackBoxGIU.jar, download the new one where the bug has been fixed.

Assignment

Write a black box specification for the front-end of a simple web browser. It will have Stop, Back, Forward, Close, and Home buttons. It will also have a URL bar from which an arbitrary web page can be requested. It interacts with a user and with whatever web servers it needs. In other words, the user can press any button or enter a URL in the URL bar, and a page can be received from a web server.

In response to the buttons, the web browser can show a recieved page, show a previous or next page in the history, request the user's homepage or some URL webpage, or cancel a request.

You should use the tool to define macros for common stimulus histories. For example, in order for the user to be able to click the back button, it will depend upon how many web pages have been visited, how many times they've pressed the back button, and how many times they've pressed the forward button. You can define a canBack macro that counts the number of stimuli that result in a page being shown, subtract from that the number of stimuli that result in the previous page being shown, and add to that the number of stimuli that result in the next page being shown. If this sum is greater than one, then the user can press the back button.

Macros you might want to define are: canBack, canForward, RequestPending, RequestMade, PageShown. Note that you can use macros within macros. For example, RequestPending can be defined as RequestPending:PageReceived.

Use BlackBoxGUI to create your black box specification. Begin by determining appropriate stimuli and responses. Then write a black box row for each situation the web browser will encounter. In general, your black box should be at a high level of abstraction. Typical responses may include the display of a web page or the issuing of an HTTP request. A solution should have about 10 rows.

Once your black box is complete, verify it using the exhaustive checker to ensure completeness and consistency. Also use the prototype tool to interactively ensure that the browser behaves properly. Pay particular attention to whether the "Forward" and "Back" buttons behave appropriately.

Save your specification as web_browser.html. Edit the file to include your name at the top.

Once you have verified the completeness, consistency, and behavior of your specification, answer the following questions in a file called writeup.txt. Be sure to include your name.

1. How many total histories did the exhaustive checker need to search in order to verify the consistency of your specification?
2. To what extent was the prototyping tool helpful in ensuring that your specification exhibited appropriate behavior?
3. To what extent did the history specification language provide you with appropriate abstractions? What additional abstraction mechanisms would have simplified the writing of the specification?
4. In general, what aspects of the user interface were helpful in completing the specification? What aspects proved to be obstacles?
5. An alternative approach to black box specification is to enumerate stimulus histories in ascending order of length, and identify equivalence classes among them. The enumeration process is complete when the addition of any additional stimulus will result in a history that fits into an already-determined equivalence class. Having used the set-based approach implemented in this tool, what advantages might the enumeration approach have? Disadvantages?
6. Compare and contrast black box specifications with one other formal method you have studied this semester. What are their relative strengths and weaknesses? For what domains or problems do they seem more or less appropriate?
7. Black box specifications force one to think in terms of previous stimulus histories rather than internal state. To what extent do you feel comfortable writing specifications in this manner?

Grading

200 points total. 50% for the writeup, 50% for the correct specification.

Email your web_browser.html and writeup.txt files to meghan@cs.wm.edu.