The complexity of designing communication protocols has lead researchers to develop various techniques for designing and verifying protocols. One of the most important techniques is a compositional technique. Using a compositional technique, a large and complex protocol is designed and verified by composing small and simple protocols which are easy to handle, design and verify. Unlike the other compositional approaches, we propose compositional techniques for simultaneously composing service specifications and protocol specifications based on Formal Description Techniques (FDTs) called LOTOS. The proposed techniques consider alternative, sequential, interrupt and parallel composition of service specifications and protocol specifications. The composite service specification and the composite protocol specification preserve the original behaviour and the correctness properties of individual service specifications and protocol specifications. We use the weak bisimulation equivalence (), to represent the correctness properties between the service specification and the protocol specification. When a protocol specification is weak bisimulation equivalent to a service specification, the protocol satisfies all the logical properties of a communication protocol as well as provides the services that are specified in the service specification.

Process algebras with name passing have been proposed for concurrent mobile processes. They can be suitable to describe dynamical changes of connections among processes. To describe mobile communication or mobile computing systems, however, it is necessary to consider locations at which processes run. We propose a description method to design mobile communication systems using a concurrent calculus in this paper. The concept of a field is introduced to model locality of communication. An extension of π-calculus with a field is proposed. The extension does not include locality represented by a field while most related works treat locality within their languages. A field is given when behavior of a target system is verified in a particular environment. The aim of the extension is to verify and to test connectivity between processes under various geographical constraints. This method could be design-oriented in this context. Equivalence relations with/without location in this calculus are also discussed.

In this paper, we consider a flexible method for designing n-entities communication protocols and services. The proposed technique considers alternative and parallel composition of n service specifications and n protocol specifications, where n 2. The specifications are specified in Basic LOTOS which is a Formal Description Technique (FDT). We use the weak bisimulation equivalence () to represent the correctness properties between the service specification and the protocol specification.

We introduce an inheritance concept into a specification method of a concurrent system in order to reuse and refine existing specifications. Reusability by inheritance is emphasized in this paper. We take multiple inheritance to enable to reuse several specifications at a time. An upper specification can be skillfully reused by dividing inherited parts and non-inherited ones if the specification contains unnecessary parts for a lower specification. As an application, we specify the FIPA contract net interaction protocol (IP) with the function of an agent authentication. This is accomplished by using multiple inheritance. We also specify the FIPA iterated contract net IP by reusing the FIPA contract net IP. We have been developing a validation support tool for specifications described with the proposed method.

In this paper an approach to formal specification and verification of ISDN services in LOTOS is presented. As for specification, it is shown that LOTOS can be effectively applied to describe different levels of ISDN service specifications. At the higher level, only the external behaviour of the network is specified. On the other hand, at the lower level, specifications include the behaviour of network components such as switching systems, where each switching system can be specified independently of each other. Such specification style, proves suitable for verification of specifications by using the concepts of the simulation relation.

In this paper, we present an automatic implementation method by which executable communication programs in C can be generated from protocol specifications in LOTOS. The implementation method consists of two parts: 1) An implementation strategy and 2) a set of translation rules. The first part consists of the basic ideas on how to realize the primary mechanisms in LOTOS specifications. The second part formulates the implementation method by way of the translation rules based on the implementation strategy. The characteristics of our method can be summarized as follows: We formulate our implementation method by way of translation rules. These rules are defined topdown in the form of syntax-directed translation function. The mechanism for controlling concurrency and communication among the user processes corresponding to the processes in LOTOS specification is easily realized by using UNIX operating system functions. The translation rules have been implemented on the AS 3000 (SUN3) workstation. An application of this implementation method is demonstrated by a simplified token-ring-protocol.

We present a topological framework of stepwise specification for concurrent systems in this paper. Some of description techniques can make topologies on the system space. Such topologies corresponds to abstract levels of those description techniques. Using a family of such description techniques, one can specify systems stepwisely. This framework allows to bridge various DTs and modularizing, so that global properties and module properties of systems become to be related to each other. Within this framework, we show derivation of a LOTOS cpecification from temporal logic formulae. An extended version of LOTOS with respect to concurrency is used in this paper. A semantics including concurrency is introduced to do this in this method. The method presented in this paper is applied to mobile telecommunication.

This paper discusses a software verification support environment Vega which is based on a model-theoretic methodology that enables verification support for the temporal properties of protocol specifications described in the formal description technique LOTOS. In the methodology of Vega, a protocol specification is defined through the LOTOS process reflecting its practical system structure. The temporal properties to be verified are given as the requirement which the protocol needs to satisfy from the viewpoint of events and are formulated by using the branching time temporal logic defined in this paper. Verification is done by determining whether or not the given temporal properties are satisfied by the model, which corresponds to the transition system derived from the LOTOS specification of the protocol. Vega is provided with an effective interface function, as well as the function of simple model checking based on the above methodology, to give some degree of flexibility for the expression of temporal properties to be verified. Specifically, it allows the user to define useful expressions by combining builtin temporal logic formulas and enter them in Vega for use at any time. With the provision of these functions, Vega is expected to serve as a very powerful and flexible verification support tool.

Users of computer communication systems and their requirements are rapidly increasing and changing. It is desirable to have a development method which helps to make small changes in a design of a system to obtain another system which satisfies new requirement changes. We propose a flexible synthesis method which adopts designers' requirement changes in formal protocol specifications designed in LOTOS.

We propose a method which can construct LOTOS specifications of communication systems from temporal properties described in Extended branching time temporal logic (EBTL) in this paper. Description of LOTOS, one of Formal Description Techniques, is based on behaviors of systems so that LOTOS permits strict expression. However, it is difficult to express temporal properties explicitly. On the other hand, Temporal logic is based on properties of systems. Thus temporal logic permits direct expression of temporal properties which can be understood intuitively. Accordingly, temporal logic is more useful than FDTs on the first step of systems specification. This method is effective in this point of view. Specifications obtained using this method can have a structured style. When temporal properties are regarded as constraints about temporal order among actions of systems, those specification can have a constraint oriented style. This method is based on sequential composition of Labelled Transition Systems (LTSs) which are semantics of LOTOS. EBTL is also defined on LTSs. In general, many LTSs satisfy the same temporal property. To obtain such the minimal LTS, the standard form of LTSs corresponding to EBTL operators are defined. Those standard LTSs are mainly tailored to the field of communication protocol. We also show conditions that original temporal properties are preserved in case of sequential composition of standard LTSs. In addition, applying this method to the Abracadabra Protocol, we show that this method can construct specifications of concrete protocols effectively.

In a distributed concurrent system such as a computer communication network, the system components communicate with each other via communication links in order to accomplish a desired distributed application. If the links are dynamically established among the components, the system configuration as well as its behavior becomes complex. In this paper, we give formal specification of such a dynamically reconfigurable system in which the components are modeled by communicating finite state machines executed concurrently with the communication links which are dynamically established and disconnected. We also present an algorithm to validate the safety and link-related properties in the specified behavior. Finally, we design and implement a simulator and a validator that enables execution and validation of the given specification, respectively.

Users of computer communication systems and their requirements are rapidly increasing and changing. In order to deal such a situation a rapid development method of communication systems is necessary. One of the such development methods is to change an existing specification of the system to obtain the desired specification of the system. However, a very little work has been done to support making changes in formal specifications. In this paper, we propose a mechanism for making changes in formal protocol specifications by adding protocol functions in an existing protocol specification.

The number of Web applications handling online transaction is increasing, but verification of the correctness of Web application development has been done manually. This paper proposes a method for modeling, verifying and testing Web applications. In our method, a Web application is modeled using two finite-state automata, i.e., a page automaton which specifies Web page transitions, and an internal state automaton which specifies internal state transitions of the Web application. General properties for checking the Web application design are presented in LTL formulae and they are verified using the model checker Spin. Test cases examining the behavior of the Web application are also generated by utilizing the counterexamples obtained as the result of model checking. We applied our method to an example Web application to confirm its effectiveness.

One of the important techniques in communication system design is the composition of service and protocol specifications. In this paper, we have presented a new approach to the composition technique based on the weak bisimulation concept. The main objective is to combine service specifications and protocol specifications individually and simultaneously. The composition technique can maintain the equivalence between the composed service and protocol specifications. LOTOS language terms are utilized to describe the communication specifications. The application on the asynchronous model is presented. Moreover, a support system of the composition technique is developed and presented in this paper.

In this paper, we clarify the properties of the contract net protocol based on its formal specification. To specify the contract net protocol, we propose a formal specification method for an agent system. In this method, agents are modeled as communicating finite state machines. To deal with the behavior of agents and its time passage explicitly, we incorporate the concept of time into the communicating finite state machine. The contract net protocol is specified based on the specification method proposed in this paper. From the specification, we analyze the possibility about agent deadlock and its avoidance solution.