# Submodule Construction for Specifications with Input Assumptions and Output Guarantees

## 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? - 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.

## Keywords

Relational Database Finite State Machine Label Transition System Communicate Sequential Process Finite State Automaton## References

- [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
- [Abit 95]S. Abiteboul, R. Hull and V. Vianu, Foundations of Databases, Add.-Wesley, 1995.Google Scholar
- [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
- [Boch 01b]G. v. Bochmann, Submodule construction-the inverse of composition, Technical Report, Sept.2001, University of Ottawa.Google Scholar
- [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 - [Broy 95]M. Broy, Advanced component interface specification, Proc. TPPP’94, Lecture Notesin CS 907, 1995, pp. 369–392.Google Scholar
- [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
- [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
- [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
- [Hoar 85]C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall, 1985.Google Scholar
- [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
- [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
- [Kim 97]T. Kim, T. Villa, R. Brayton, A. Sangiovanni-Vincentelli. Synthesis of FSMs: functional optimization. Kluwer Academic Publishers, 1997.Google Scholar
- [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
- [Maie 83]D. Maier, The Theory of Relational Databases, Computer Science Press, Rockville, Maryland, 1983.zbMATHGoogle Scholar
- [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
- [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
- [Parr 89]J. Parrow, Submodule Construction as Equation Solving in CCS, Theoretical Computer Science, Vol. 68, 1989.Google Scholar
- [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
- [Petr 98]A. Petrenko and N. Yevtushenko, Solving asynchronous equations, in Proc. of IFIP FORTE/PSTV’98 Conf., Paris, Chapman-Hall, 1998.Google Scholar
- [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
- [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
- [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
- [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