Recent publications - in the area of formal specifications
Synthesis of Communication Systems - Tutorial given at Concordia Summerschool,
Aug. 2002
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