The functions of the support tools

The functions of the support tools are as follows.

UML diagram management component

UML diagram management component manages UML diagrams of the target domain. It provides the following functions:

1. the function for storing a UML diagram,

2. the function for deleting a stored UML diagram, 3. the function for searching a selected UML diagram,

4. the function for making the list of the stored UML diagrams,

5. the function for making the list of the component names occurring in the stored UML diagrams,

6. the function for generating the information about unverified properties, 7. the function for changing the information about verified properties,

8. the function for generating the information about ungenerated connectors, and 9. the function for changing the information about generated connectors.

Consistency verifier component

Consistency verifier component verifies the consistency of the stored UML diagrams. To verify the consistency, firstly, it translates UML diagrams into CafeOBJ specifications.

Then, it generates verification scripts for the consistency verification. Finally, by sending theCafeOBJspecifications and the verification scripts to theCafeOBJverification system, it verifies the consistency. It provides the following functions:

1. the function for translating the stored UML diagrams into CafeOBJspecifications, 2. the function for generating the verification scripts of refinement verification about

business model,

3. the function for generating the verification scripts of refinement verification about component specification,

4. the function for generating the verification scripts of verification of satisfaction of static invariants,

5. the function for manipulating the CafeOBJ verification system, and

6. the function for supporting the verification that uses the verification scripts written by users.

Connector generator component

Connector generator component for the tool for SAgenerates function beans and interface beans corresponding to connectors from the verifiedCafeOBJverification. It provides the following functions:

1. the function for generating function beans and 2. the function for generating interface beans.

Connector generator component for the tool for CS generates function beans and in-terface servlets corresponding to connectors from the verified CafeOBJ verification. It provides the following functions:

1. the function for generating function beans and 2. the function for generating interface servlets.

Component library management component Component library management component manages

1. components that provides basic functionalities of the target domain and 2. connectorsthat are generated by connector generator component.

It provides the following functions:

1. the function for storing a component,

2. the function for deleting a stored component, 3. the function for searching a selected component,

4. the function for making the list of the stored components’ names, 5. the function for storing a connector,

6. the function for deleting a stored connector,

7. the function for searching a selected connector, and

8. the function for making the list of the stored connectors’ names.

Software generator component

Software generator component, firstly, generates the target software by combining compo-nents and connectors that are stored in component library management component, then, collect the binary files of the software as the archive, finally, send the archive to users. It provides the following functions:

1. the function for generating the target software,

2. the function for collecting the binary files of the software as the archive, and 3. the function for sending the archive.

Exclusion control component

Exclusion control component controls concurrent accesses to stored UML diagrams from some users. It provides the following functions:

1. the function for checking whether the selected UML diagrams can be changeable and

2. the function for changing the management information of the UML diagrams.

It decides whether the selected UML diagrams can be changeable based on the manage-ment information.

User interface component

User interface component mediates between users and the other components. It provides the following functions:

1. the function for selecting an user interface screen depending on a situation and 2. the function for controlling the other components to execute a user request.

Chapter 12 Case Studies

We did case studies:

1. of the domain of file transfer programs and 2. of the domain of online bookstores.

12.1 The Domain of File Transfer Programs

We did a case study of the domain of file transfer programs by using the support tool of CBDL using LFMB.

The software family of the domain includesPUT-Athat transfers A’s files on the local machine to a remote machine and GET-B that transfers B’s files on a remote machine to the local machine. The component library is divided into FTP group that transfers files and INFO group that manages personal information, like user names and passwords (Fig. 12.1). FTPftp and FTPcopyprovide file transfer functions using FTP protocol and using copy command of OS, respectively. FTPftp and FTPcopy belong to FTP group.

INFO-AandINFO-Bprovide management functions of A’s personal information and B’s personal information, respectively. INFO-Aand INFO-Bbelong to INFOgroup. PUT-A is constructed from FTPftp, INFO-A, and the connector of PUT. GET-Bis constructed fromFTPftp, INFO-B, and the connector of GET.

We developed INFO-A and INFO-B from scratch. But, we developed FTPftp and FTPcopy by using the free software providing functions about FTP protocol and copy command of OS, respectively. By developing “the lappers” and by combining them with the existing software, we developed FTPftp and FTPcopy.

We developed PUT-A as follows. Firstly, we prepared the component library with CafeOBJspecifications. Secondly, we input

1. the primitive component specification that specifies behavior of PUT group and 2. the component specification that specifies how to combine FTP group and INFO

group to develop the PUT group

into the tool. Then, we selected FTPftp and INFO-A on the tool. Finally, the tool verified refinement and generatedPUT-A whose correctness is assured by the refinement verification (Fig. 12.2).

Through this case study, we show that:

Connector of PUT

Connector of GET FTPftp INFO-A

FTPftp INFO-B PUT-A

GET-B

Component library Group Component

FTP INFO

FTPftp,FTPcopy INFO-A,INFO-B

Figure 12.1: The software family and the component library

Figure 12.2: The outlook of PUT-A component

1. for the small domain, the support tool is useful for generating components whose correctness is assured and

2. we can develop components of the component library by using existing software.