ASTRAL Examples

Bakery Algorithm

[see the ASTRAL specification]

The bakery algorithm specification describes the distributed mutual exclusion algorithm of [Lam 74], which is shown below. Each of n processes is involved in a computation that contains a "critical region", which only a single process may enter at any given time. The process that is to enter its critical region determines if it is permissible to do so by checking the status of its "siblings". The critical requirement of the system is that only one process will be in its critical region at any given time.

boolean choosing[n] = {false, ..., false};  
integer number[n] = {0, ..., 0};  

while (true) {  
	choosing[my_process_id] = true;  
	number[my_process_id] = maximum(number[1], ..., number[n]) + 1;  
	choosing[my_process_id] = false;  
	for (integer j = 1; j <= n; j++) {  
		while (choosing[j])  
			{}  
		while (number[j] != 0 &&  
			number[j] <= number[my_process_id] &&  
			(number[j] != number[my_process_id] || j < my_process_id))  
			{}  
	}  
	critical_section();  
	number[my_process_id] = 0;  
	noncritical_section();  
}  

Cruise Control

[see the ASTRAL specification]

The cruise control system is based on the description in [WM 85]. The system is an automatic throttle control system for an automobile. The driver engages the system at a desired speed and the controller continuously adjusts the throttle according to fluctuations in terrain, etc. that have an effect on the speed of the vehicle. The system consists of four processes. A tire sensor keeps track of the number of times the wheels have rotated. A speedometer computes the current speed of the vehicle based on the number of wheel rotations and the sample rate. An accelerometer computes the current acceleration of the vehicle based on the speed and the sample rate. The controller itself consists of the cruise interface, the accelerator and brake pedals, and the throttle control. When the controller is maintaining speed, the actual throttle will always be the higher of the throttle that the driver is demanding with the accelerator pedal and the throttle that the controller is attempting to set. The cruise control must be disabled as quickly as possible when the brake pedal is applied.

Elevator Control System

[see the ASTRAL specification]

The elevator system was adapted from a description in [FF 84] as shown in the figure below. An N story building is serviced by the elevator. A panel of N buttons is located inside the elevator car to request that the elevator move to a given floor. Each floor in the building also has a button panel, which has an up and a down button to request that the elevator stop at the floor and move in the corresponding direction. The elevator must service all the requests in one direction before it can move in the opposite direction. When the elevator arrives at a floor en route to another destination and no request has been made inside the elevator for that floor, nor has a request been made at that floor's button panel for movement in the same direction, the elevator continues on to its next destination without stopping or opening the door. If such a request has been made, however, then the elevator stops and opens the door. The door is always opened for a duration of t_stop at which point it closes. When the elevator arrives at a floor that is the last request in its direction of movement, the door opens and then its behavior depends on the situation in the building. If the button panel at the elevator's location has requested movement in the same direction, the user must get in and push the desired floor on the elevator's button panel before the door has finished closing. Otherwise, the elevator is free to move in the opposite direction to service another request, if one exists. The critical timing requirement of the elevator system is that the elevator must service any request within t_service_request time of when the button was pushed.

Olympic Boxing Scoring System

[see the ASTRAL specification]

In Olympic boxing, each bout consists of three 3-minute rounds, with a 1-minute interval between rounds. In 1992, the Olympic Committee decided to use an electronic scoring system for boxing. The following is a description of the system taken from the official 1996 Olympic web site [Oly 96].

"For the first time in Olympic boxing competition, an electronic scoring system was used at the 1992 Olympic Games in Barcelona, Spain. Under electronic scoring, five working judges are positioned at ringside with a desk-mounted keypad at each judge's position.

The keypads, each of which are linked to the mainframe computer at the jury table, feature four buttons--red and blue scoring and red and blue warning buttons.

During the course of the bout, judges record scoring blows for each competitor on their keypad. In order for a blow to be recorded by the computer as part of the official (or combined/accepted score), three of five judges must press the same colored button within a one-second interval. The one-second interval begins when the first judge records a blow.

Scores are reported in terms of number of blows recognized by a majority of judges over the course of the three rounds combined."

The specification in appendix A only considers the scoring portion of the system (i.e. warnings are not included).

Phone System

[see the ASTRAL specification]

The phone system description and specification was taken from [CGK 97]. The system consists of a set of phones that need various services (e.g. getting a dial tone, processing digits entered into the phone, making a connection to the requested phone, etc.) as well as a set of central control centers that perform the services. Each control center is responsible for the phones belonging to its area, and it is provided with all the functionality needed to set up a local call. Control centers are also intended to deal with long distance calls (i.e. calls to other areas). Calls to outside areas are modeled by exported variables (i.e. the data is sent to the external environment), while calls from an outside area are modeled as exported transitions (i.e. they are the information provided in the parameters of a call to an exported transition from the external environment). The example is a simplification of a real phone system. Every local phone number is seven digits long, area codes are three digits long, a customer can be connected to at most one other phone (either local or in another area), and ongoing calls cannot be interrupted. The main requirement of the system is that phones will be given a dial tone within two seconds.

Production Cell

[see the ASTRAL specification]

The production cell specification is based on the description in [LL 95] and is shown in the figure below. The purpose of the production cell is to forge metal blanks and convey them to a stockpile. Each blank is added to a feed belt that is continuously moving until a light sensor at the end of the belt detects a blank. The feed belt then stops. When the elevating rotary table at the end of the belt is in the proper position, the feed belt moves the blank onto the table and continues operation until another blank reaches the sensor. Once a blank is on the table, the table elevates to the level of a robot arm and rotates into the appropriate position. The robot consists of two stationary arms, each of which is positioned at a different vertical position. The robot assembly can be rotated and each arm can extend and retract to pickup and drop metal plates. The first arm picks up blanks from the table and rotates to deliver them to a press. The press forges the blank into a plate, which is then picked up by the second robot arm and delivered to a deposit belt. Like the feed belt, the deposit belt is continuously moving until a light sensor at the end of the belt detects a plate. The belt then stops and waits until the plate is removed by a crane, which transports the plate to a stockpile. The main requirements of the system are that the robot arms do not collide with any of the other pieces of equipment, and that the blanks and plates are only dropped at the proper places and never onto another blank or plate.

Railroad Crossing

[see the ASTRAL specification]

The railroad crossing system is based on the description in [HL 94]. The system consists of a set of railroad tracks that intersect a street by which cars may cross the tracks. A gate is located at the crossing to prevent cars from crossing the tracks when a train is near. A sensor on each track detects the arrival of trains on that track. The region between the sensors and the crossing exit is denoted by R and the crossing, which is a subinterval of R, is denoted by I. The figure below illustrates the railroad crossing with two train tracks. The critical requirements of the system are that whenever a train is in I, the gate must be down and when no train has been in R for a reasonable length of time, the gate must be up.

Stoplight Control System

[see the ASTRAL specification]

The stoplight specification is for a four-way intersection in which each direction has its own turn lane. This example was adapted from a stoplight system described in [FF 84]. The figure below depicts the intersection of the system. Each direction has two signals. The "arrow" signal is the signal for the left turn lane and the "circle" signal is the signal for going straight and for right turns. The signals can change independently; thus, for example, if the circle of direction one is green, it is not necessarily the case that the circle opposite of direction one is green. The controller can therefore act "intelligently", such as changing both the arrow and the circle of a direction to green at the same time if no car is in the turn lane of the opposite direction.

One direction is designated as the "main direction" and is assumed to be the direction with the most traffic flowing. The controller will keep the circle and arrow of the main direction green when no cars are waiting at the intersection.

The system makes no assumptions about the behavior of cars, thus a car can sit on a sensor forever and the controller will still cycle the directions with the green appropriately. A direction will stay green for at least min_green time and yellow for at least min_yellow, and a car will wait no longer than max_wait for a green.

Related Publications

[Kol 99d]

[Kol 99b]

References

URL: http://www.cs.ucsb.edu/~astral/examp.html
last update: 7-27-99