Recent publications - in the area of formal specifications

Synthesis of Communication Systems - Tutorial given at Concordia Summerschool, Aug. 2002

• The slides

A formal method for synthesizing optimized protocol converters and its application to mobile data networks

• Authors: Z. Tao, G. v. Bochmann and R. Dssouli
• Reference: [Tao 97a] Mobile Networks & Applications, vol.2, no.3, 1997, pp.259-69. Publisher: Baltzer; ACM Press, Netherlands.
• Abstract: As mobile information networks are expanding rapidly, we expect to integrate voice, paging, electronic mail and other wireless information services. Interworking units that perform protocol conversion at the boundaries of different networks will play an important role. In this paper, we propose an efficient algorithm for constructing optimized protocol converters to achieve interoperability between heterogeneous data networks. This algorithm first derives constraints from two given protocols, and applies the constraints to channel specifications, thus removing message sequences that do not contribute to system progress. Then, an optimized converter is generated from a given service specification, the two protocol specifications and the modified channel specifications. A reduction relation is used to compare the service specification and the constructed internetworking system in order to deal with the problem of nondeterministic services. Compared with related works, our method has two advantages: (1) it generates an optimized converter; (2) it can be applied to the case that the service specification is nondeterministic. The application of the method to mobile networks is given by an example. (22 References).
• For a copy, see journal

Submodule construction and supervisory control: a generalization

• Authors: G. v. Bochmann
• Reference: [Boch 01a] in Proc. of Int. Conf. on Implementation and Applications of Automata (invited paper), to be published as Springer Lecture Notes.
• Abstract: We consider the following problem: For a system consisting of two submodules, the behavior of one submodule is known as well as the desired behavior S of the global system. What should be the behavior of the second submodule such that the behavior of the composition of the two submodules conforms to S ? - This problem has also been called "equation solving", and in the context of supervisory control, it is the problem of designing a suitable controller (second submodule) which controls a given system to be controlled (first submodule). Solutions to this problem have been described by different authors for various assumptions about the underlying communication mechanisms and conformance relations. We present a generalization of this problem and its solution using concepts from relational database theory. We also show that several of the existing solutions are special cases of our general formulation.
• For a copy click here: PDF

Submodule construction - the inverse of composition

• Authors: G. v. Bochmann
• Reference: [Boch 01b] Technical Report, Sept. 2001, University of Ottawa.
• Abstract: We consider the following problem: For a system consisting of two submodules, the behavior of one submodule is known as well as the desired behavior S of the global system. What should be the behavior of the second submodule such that the behavior of the composition of the two submodules conforms to S ? - This problem has also been called "equation solving", and in the context of supervisory control, it is the problem of designing a suitable controller (second submodule) which controls a given system to be controlled (first submodule). Solutions to this problem have been described in the context of various specification formalisms and various conformance relations. This paper presents a generalization of this problem and its solution in the context of relational databases, and shows that this general solution can be used to derive several of the known algorithms that solve the problem in the context of regular behavior specifications based on finite state machines with synchronous communication or interleaving semantics. The paper also provides a new solution formula for the case that the module behaviors are specified in a hypothesis-guarantee paradigm and distinguish between input and output interactions. In the sub-case of regular behavior specifications and interleaving semantics, this solution formula gives rise to an algorithm for Input/Output Automata, which is similar to one published recently. The formula also applies to the case of synchronous communication, which was not considered before.
• For a copy click here: PDF

Submodule construction for systems of I/O automata

• Authors: J. Drissi and G. v. Bochmann
• Reference: [Dris 99b] submitted for publication
• Abstract: This paper addresses the problem of designing a submodule of a given system of communicating I/O automata. The problem may be formulated mathematically by the equation (C||X)rA under the constraint IX=In, where C represents the specification of the known part of the system, called the context, A represents the specification of the whole system, X represents the specification of the submodule to be constructed, || is a composition operator, r is a conformance relation and In is the required set of inputs for X. As conformance relation, we consider the safe realization and the subtype relation. The subtype relation is a generalization of the well known criteria of trace equivalence, complete trace equivalence, quasi equivalence and reduction, while the weaker safe realization relation is implied by all those criteria. We propose two algorithms for solving the problem with respect to the safe realization and the subtype relation and we characterize the set of solutions in each case.
• For a copy click here: PDF

Submodule construction tool

• Authors: J. Drissi and G. v. Bochmann
• Reference: [Dris 99a] in Proc. Int. Conf. on Computational Intelligence for Modelling, Control and Automation, Vienne, Febr. 1999, (M. Mohammadian, Ed.), IOS Press, pp. 319-324.
• Abstract: Using the programming language Java, we developed the Submodule Construction Tool, which implements algorithms for the submodule construction problem. The submodule construction problem (SCP) is to construct the specification of a submodule X when the specification of the system and all submodules but X are given. This problem is encountered in the hierarchical design of complex systems, in the synthesis of controllers and in the reuse of components. The tool requires a number of files as input and produces a file containing the result. For the input/output Finite State Machine model, we can obtain the generic solution, the minimal solution with respect to the number of states, we can check if a given FSM is a solution and we can find the minimal reduction of a given observable nondeterministic FSM. For the I/O automata model, we can find the generic solution for the safe realization relation and the subtype relation, we can check if a given I/O automaton is a safe realization or a subtype of another I/O automaton, we can compose I/O automata, we can find the resulting I/O automaton after hiding a subset of the alphabet and finally we can obtain the minimal trace equivalent I/O automaton.
• For a copy click here: PDF

Protocol re-synthesis with optimal allocation of resources based on extended Petri nets

• Authors: H. Yamaguchi, K. El-Fakih, G. v. Bochmann and T. Higashino
• Reference: [Yama 01a] submitted for publication (DC)
• Abstract: Protocol synthesis is used to derive a speci cation of a distributed system called a protocol specication (a set of programs of cooperative computers) from a speci cation of services (called a service speci cation) to be provided by the distributed system to its users. It reduces design costs and errors in specifying communications between computers in the protocol speci cation. In general, maintaining such a distributed system involves applying frequent minor modi cations to the service speci cation due to changes in the user requirements. Deriving a protocol speci cation after each modi cation using the existing synthesis methods is considered expensive and time consuming. Moreover, we cannot identify what changes we should make to the protocol speci cation for the modi cation to the service speci cation. In order to reduce the maintenance cost of such asystem, we present a new synthesis method to re-synthesize only the corresponding part of the current protocol speci cation after modi cations to the service speci cation. The method consists of a set of simple rules that are applied to the protocol speci cation written in an extended Petri net model. An application example is given along with some experimental results.
• For a copy click here: PDF

Automatic derivation of Petri-net based distributed specification with optimal allocation of resources

• Authors: H. Yamaguchi, K. El-Fakih, G. v. Bochmann and T. Higashino
• Reference : [Yama 00b] Proc. of IEEE Int. Conf. on 15th IEEE Int. Conf. on Automated Software Engineering (ASE'2000), Grenoble, France, Sept. 2000, pp.
• Abstract:
• For a copy click here: PDF

Protocol re-synthesis based on extended Petri nets

• Authors: K. El-Fakih, H. Yamaguchi, G. v. Bochmann and T. Higashino
• Reference: [ElFa 00b] Proc. of Workshop on Software Engineering and Petri Nets (SEPN-2000), June 2000, Aarhus, Denmark.
• Abstract: Protocol synthesis is used to derive a speci cation of a dis- tributed system from the speci cation of the services to be provided by the system to its users. Maintaining such a system involves applying frequent minor modi cations to the service speci cation due to changes in the user requirements. In order to reduce the maintenance costs of such a system, we present an original method that consists of a set of rules that avoid complete protocol synthesis after these modi cations. These rules are given for a system modeled as an extended Petri net. An application example is given along with some experimental results.
• For a copy click here: PDF

A Petri net based method for deriving distributed specifications with optimal allocation of resources

• Authors: H. Yamaguchi, K. El-Fakih, G. v. Bochmann and T. Higashino
• Reference : [Yama 00a] Proc. of Int. Conf. on Software Eng. Applied to Networking and Parallel/Distr. Computing (SNPD'00), May 2000, Reims, France, pp.19-26.
• Abstract: In this paper, we present a method for the synthesis of ex-tended Petri net based distributed specification. Although a lot of synthesis methods have been proposed, only a few syn-thesis methods have treated resources (computational data) such as databases and files. In contrast to previous meth-ods that assume some fixed resource allocation, our method finds an optimal resource allocation that optimizes the de-rived distributed specification, based on some reasonable communication cost criteria. The method starts by identi-fying the set of rules for deriving a protocol specification from a given service specification. Based on these rules, an optimal resource allocation problem is formulated using an integer linear programming model. An example application is discussed.
• For a copy click here: PDF

A method and a generic algorithm for deriving protocols for distributed applications with minimum communications cost

• Authors: K. El-Fakih, H. Yamaguchi and G. v. Bochmann
• Reference: [Elfa 99a] Proc. Int. Conf. on Parallel and Distr. Computing and Systems, Nov. 1999, Boston, USA .
• Abstract: We consider a set of rules for deriving the specification of the protocol of a distributed system from a given specification of services, and define and formulate the message exchange optimization problem using a 0-1 integer programming model. This problem is about determining the minimum number of messages to be exchanged between the physical locations of the distributed system, in order to reduce the communication cost. We then present a genetic algorithm for solving this problem. The main advantage of this algorithm, in comparison with exact algorithms, is that its complexity remains manageable for realistic large specifications. The experimental results show that the minimum number of messages to be exchanged is found in a very reasonable time.
• For a copy click here: PDF

Protocol synthesis for real-time applications

• Authors: A. Koumsi, G. v. Bochmann and R. Dssouli
• Reference : [Khou 99a] in Proc. Int. Conf. on Formal Description Techn. for Distributed Systems (FORTE/PSTV), Oct. 1999, Beijing (accepted for publication)
• Abstract:
• For a copy click here: PDF

Object composition: a case study

• Authors: D. Ramazani and G. v. Bochmann
• Reference: [Rama 99a] Proc. IFIP Workshop on Formal Methods for Open Object-based Distributed Systems (FMOODS), Italy, 1999,
• Abstract:
• For a copy click here: PDF