This paper proposes a protocol verification tool where protocols are described in an extended Petri net and Horn clauses. The extended net model contributes to reduce state space in verification with hierarchical description. The model also includes timed and colored net. Horn clause enables protocol designers to grasp a protocol by the declarative semantics. They can describe non critical but mandatory portion of a protocol like error processing or abortion with Horn clauses. Protocols are verified through simulation. Protocol verification includes two methods, all-in-one and hierarchical methods. By the all-in-one method all description is translated into Prolong clause and simulated exhaustively, whereas by the hierarchical verification, simulation begins with the lowest layer and deduces sufficient conditions that give liveness and safeness of the net model. Then the layer is replaced by a simpler net model that is incorporated into the higher layer. The scheme is applied to an illustrative example of the Alternating Bit protocol to discuss its effectiveness.

In this paper, we propose the architecture of BALANCE (Better Adaptive Load-balancing through Acquiring kNowledge of Characteristic of an Environment) in which users can submit their jobs without acquiring either a status of an environment or characteristics of jobs and servers even in a widely connected heterogeneous network. The architecture of BALANCE includes three types of information bases and two types of daemons. Information bases, namely job, resource, and environment information base, manage the knowledge of job characteristics, available resources for CPUs, and status of the environment, respectively, as a proxy for users. The dispatching daemon selects an adequate server for each job using knowledge stored in the information bases. A service daemon executes each job. On completing each job, a service daemon gets a statistic of the job and returns it to the dispatching daemon where the job came from so that the statistic will be available at the next dispatching time. BALANCE enables an environment (1) to balance the load, (2) to share software functions as well as hardware facilities, and (3) to learn a user's job characteristics. We have implemented a prototype with more than 50 heterogeneous UNIX workstations connected by different networks. Two simple experiments on this prototype are presented. These experiments show a load balancing scheme that takes the characteristics of each job into account.

A program slice is a set of program statements that directly or indirectly contribute to the values assumed by a set of variables at some program execution point. A few slicing algorithms have proposed to far but none of them are considered from the viewpoint of program modification. In this paper, we define a variable dependence graph (VDG) and show a new slicing algorithm on VDG. We also compare the time complexity of the algorithm with that of other existing algorithms and discuss the suitableness of our algorithm for program modification. As the result of this, we argue our algorithm is suitable for embedding debugging systems.