Submodule Construction for Specifications with Input Assumptions and Output Guarantees

  • Gregor v. Bochmann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2529)


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? - Solutions to this problem have been described in the context of various specification formalisms and various conformance relations. Here we present a generalization of this problem and its solution in the context of relational databases, and show 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 automata 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 distinguishing between input and output. A new submodule construction algorithm for synchronous, partially defined input/output automata is also given.


Relational Database Finite State Machine Label Transition System Communicate Sequential Process Finite State Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [Abad 95]
    M. Abadi and L. Lamport, Conjoining specifications, ACM Transactions on Programming Languages & Systems, vol.17, no.3, May 1995, pp. 507–34.CrossRefGoogle Scholar
  2. [Abit 95]
    S. Abiteboul, R. Hull and V. Vianu, Foundations of Databases, Add.-Wesley, 1995.Google Scholar
  3. [Boch 80d]
    G. v. Bochmann and P. M. Merlin, On the construction of communication protocols, ICCC, 1980, pp.371–378, reprinted in “Communication Protocol Modeling”, edited by C. Sunshine, Artech House Publ., 1981; russian translation: Problems of Intern. Center for Science and Techn. Information, Moscow, 1981, no. 2, pp. 146–155.Google Scholar
  4. [Boch 01b]
    G. v. Bochmann, Submodule construction-the inverse of composition, Technical Report, Sept.2001, University of Ottawa.Google Scholar
  5. [Boch 02a]
    G. v. Bochmann, Submodule construction and supervisory control: a generalization, to appear in Proc. of Int. Conf. on Implementation and Applications of Automata (invited paper), August2001, Pretoria, South Africa, to be published as Springer Lecture Notes.Google Scholar
  6. [Broy 95]
    M. Broy, Advanced component interface specification, Proc. TPPP’94, Lecture Notesin CS 907, 1995, pp. 369–392.Google Scholar
  7. [Dris 99a]
    J. Drissi and G. v. Bochmann, Submodule construction tool, in Proc. Int. Conf. on Computational Intelligence for Modelling, Control and Automation, Vienne, Febr. 1999, (M. Mohammadian, Ed.), IOS Press, pp. 319–324.Google Scholar
  8. [Dris 00]
    J. Drissi and G. v. Bochmann, Submodule construction for systems of timed I/O automata, submitted for publication, see also J. Drissi, PhD thesis, Univ. of Montreal, March 2000 (in French).Google Scholar
  9. [Hagh 99]
    E. Haghverdi and H. Ural, Submodule construction from concurrent system specifications, Information and Software Technology, Vo. 41 (1999), pp. 499–506.CrossRefGoogle Scholar
  10. [Hoar 85]
    C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall, 1985.Google Scholar
  11. [Kele 94]
    S. G. H. Kelekar, Synthesis of protocols and protocol converters using the submodule construction approach, Proc. PSTV, XIII, A. Danthineet al (Eds), 1994.Google Scholar
  12. [Kim 72]
    J. Kim, and M.M. Newborn, The simplification of sequential machines with input restrictions, IRE Trans. on Electronic Computers. December, 1972, pp. 1440–1443.Google Scholar
  13. [Kim 97]
    T. Kim, T. Villa, R. Brayton, A. Sangiovanni-Vincentelli. Synthesis of FSMs: functional optimization. Kluwer Academic Publishers, 1997.Google Scholar
  14. [Lync 89]
    N. A. Lynch and M. R. Tuttle, An introduction to input/output automata, CWI Quarterly, 2(3), 1989, pp. 219–246.zbMATHMathSciNetGoogle Scholar
  15. [Maie 83]
    D. Maier, The Theory of Relational Databases, Computer Science Press, Rockville, Maryland, 1983.zbMATHGoogle Scholar
  16. [Merl 83]
    P. Merlin and G. v. Bochmann, On the Construction of Submodule Specifications and Communication Protocols, ACM Trans. on Programming Languages and Systems, Vol. 5, No. 1 (Jan. 1983), pp. 1–25.zbMATHCrossRefGoogle Scholar
  17. [Misr 81]
    J. Misra and K. M. Chandy, Proofs of networks of processes, IEEE Tr. on SE, Vol. SE-7(July1991), pp. 417–426.Google Scholar
  18. [Parr 89]
    J. Parrow, Submodule Construction as Equation Solving in CCS, Theoretical Computer Science, Vol. 68, 1989.Google Scholar
  19. [Petr 96a]
    A. Petrenko, N. Yevtushenko, G. v. Bochmann and R. Dssouli, Testing in context: framework and test derivation, Computer Communications Journal, Special issue on Protocol engineering, Vol. 19, 1996, pp.1236–1249.CrossRefGoogle Scholar
  20. [Petr 98]
    A. Petrenko and N. Yevtushenko, Solving asynchronous equations, in Proc. of IFIP FORTE/PSTV’98 Conf., Paris, Chapman-Hall, 1998.Google Scholar
  21. [Qin 91]
    H. Qin and P. Lewis, Factorisation of finite state machines under strong and observational equivalences, J. of Formal Aspects of Computing, Vol. 3, pp. 284–307, 1991.CrossRefGoogle Scholar
  22. [Rama 89]
    P. J. G. Ramadge and W. M. Wonham, The control of discrete event systems, in Proceedings of the IEEE, Vo. 77, No. 1 (Jan. 1989).Google Scholar
  23. [Yevt 01a]
    N. Yevtushenko, T. Villa, R. Brayon, A. Petrenko, A. Sangiovanni-Vincentelli. Synthesis by language equation solving (exended abstract), in Proc.of Annual Intern.workshop on Logic Synthesis, 2000, 11–14; complete paper to be published in ICCAD’2001; see also Solving Equations in Logic Synthesis, Technical Report, Tomsk State University •,• 1999, 27p. (in Russian).Google Scholar
  24. [Zafi 80]
    P. Zafiropulo, C. H. West, H. Rudin and D. D. Cowan, Towards analyzing and synthesizing protocols, IEEE Tr. Comm. COM-28, 4 (April 1980), pp. 651–660.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Gregor v. Bochmann
    • 1
  1. 1.School of Information Technology and Engineering (SITE)University of OttawaCanada

Personalised recommendations