2.4 Example: The Year 2000 Concern

The following example shows how formal verification methods can be used to solve a very simple version of the Year 2000 concern. The example is intentionally quite simple, but can be modified to show off many of the formal constraint propagation capabilities of ZD.

One of the advantages of a functional representation is that it is possible to describe a system before its design is complete, and still reap gains from the formalism proportionate to the amount of information available for the design. In this example, we pick up the design scenario part way into the design process. The system has two classes of users; employees, who have capabilities on their own workstations for tracking time, and a single Time Account Manager, who collects time reports from all employees and integrates the information into the corporate-level accounting. At this point in the design process, certain decisions have been made:

• part of the system will be responsible for allowing an employee to record the amount of time spent on different jobs. This capability has been adapted from public domain code (source code is available),
• the system will be able to save timecard information to a file in a standard format,
• part of the system will perform time accounting functions. This is based on a commercially available product that provides the necessary accounting services,
• the time accounting software provides a service for reading timecard information from a file in a standard format, and
• these two devices will communicate through file exchange, in one of the formats acceptable to the commercial accounting package.

The details of the file transfer facility have not yet been decided; in particular, we have not decided if the two systems will run in a shared file space, or use a network protocol (say, SMTP or FTP) to exchange files.

We describe this design by identifying three devices; an overall device, called IOP, which coordinates two other devices, which we call TIMEFLIES and TIMECARD. Figures 1 and 2 show an excerpt of the ZD formalism that describes this decomposition. The viewpoint taken by this decomposition is particularly suited to dealing with concerns about the communication between the employee timekeeping and the account manager time calculations. In this example, we will use this to express year 2000 constraints on the various devices. We cannot give a complete description of the formalism in this short paper, but we can describe how the particulars of this example appear in the formal ZD description.

ZD represents devices in terms of the Services they provide. A Service is specified as a number of functions. In ZD, functions are specified in terms of preconditions and postconditions, which are indicated in the formalism with the keywords If and ToMake respectively. The clauses after the keywords If and ToMake are expressed in the language of the Boyer-Moore theorem prover NQTHM [BM88]. In the figures, we can see Service specifications (ServiceSpec) for three devices, IOP, TIMEFLIES and TIMECARD. There is no Service specified for the file transfer medium, since that has not been designed yet.

Much of the information about types and unification has been left out of figures 1 and 2. Of the remaining formalism, the greatest interest for this example is the annotated finite state diagram annoted by (1) in the figure. This shows how the IOP device coordinates devices in three roles, namely the roles RECORDING-SYSTEM, MEDIUM and ACCOUNTING-SYSTEM. The diagram shows that in order for the IOP to work as specified, it will have to call upon the EXPORT function of the RECORDING-SYSTEM, the TRANSFER function of the MEDIUM, and the IMPORT function of the ACCOUNTING-SYSTEM. Finally, from the line labeled (2) onwards, we see that the TIMECARD device will fill the RECORDING-SYSTEM role, and that the TIMEFLIES device will fill the ACCOUNTING-SYSTEM role.

Given this functional decomposition, ZD provides a number of mechanisms for describing constraints among the various devices. We will describe only one of them here.

In each of the four lines labeled (3), we see a clause introduced by the keyword Provided. This indicates a precondition of the function that is to be interpreted dynamically, that is, the function annotated with a Provided clause will provide the specified functionality, provided that the condition holds in the context when the functionality is required. In this case, the proviso gives information about the year 2000 assumptions of each of the constituent devices.

ZD's proviso propagation mechanism maps these conditions to the corresponding roles in the state diagram shown by (1). It then propagates them backwards, making any necessary substitutions of variables required by the state changes expressed in the finite state diagram. In this simple example, the proviso year-precision(data) < 100 of the function IMPORT of the role ACCOUNTING-SYSTEM is propagated backwards; the IMPORT function will be achieved as specified just whenever the data has the appropriate property. The function EXPORT of the role RECORDING-SYSTEM also places a constraint on the year-precision( data); namely, year-precision(data) < 10000. Since this condition is strictly stronger than the IMPORT condition, ZD continues propagating with only the stronger condition. When ZD reaches the front of the finite state diagram in (1), it is in a position to state that this explanation for how the roles will be coordinated will work as specified, just in case year-precision(data) < 100. Since this state diagram is the explanation for the SUBMIT function of the IOP service, ZD places this condition as a proviso on that function. If the IOP were to play a role in a larger device, this proviso would be propagated further.

 

Figure 1: Time accounting example in the ZD formalism.  

 

Figure 2: Time accounting example in the ZD formalism.