This Article 
 Bibliographic References 
 Add to: 
A Decomposition of a Formal Specification: An Improved Constraint-Oriented Method
March/April 1999 (vol. 25 no. 2)
pp. 258-273

Abstract—In this paper, the authors propose a decomposition method for a formal specification that divides the specification into two subspecifications composed by a parallel operator. To make these specification behaviors equivalent before and after decomposition, the method automatically synthesizes an additional control specification, which contains the synchronization information of the decomposed subspecifications. The authors prove that a parallel composition of the decomposed subspecifications synchronized with the control specification is strongly equivalent with the original (monolithic) specification. The authors also write formal specifications of the OSI application layer's association-control service and decompose it using their method as an example of decomposition of a practical specification. Their decomposition method can be applied to top-down system development based on stepwise refinement.

[1] M. Aoyama, “Concurrent-Development Process Model,” IEEE Software, July 1993, pp. 46-55.
[2] R.L. Probert and K. Saleh, "Synthesis of Communication Protocols: Survey and Assessment," IEEE Trans. Computers, vol. 40, no. 4, pp. 468-476, 1991.
[3] C.A. Vissers, G. Scollo, M. van Sinderen, and E. Brinksma, "Specification Styles in Distributed Systems Design and Verification," Theoretical Computer Science, vol. 89, pp. 179-206, 1991.
[4] ISO, "Information Processing Systems—Open Systems Interconnection—Basic Reference Model," ISO 7498, 1984.
[5] ISO, "Information Processing Systems—Open Systems Interconnection—LOTOS—A Formal Description Technique Based on the Temporal Ordering of Observational Behavior," ISO 8807, 1989.
[6] F. Khendek, G. von Bochmann, and C. Kant, "New Results on Deriving Protocol Specifications from Service Specifications," Proc. SIGCOM '89 Symp. Comm. Architectures&Protocols, Computer Communications Review, vol. 19, no. 4, pp. 136-145, 1989.
[7] T. Higashino, "Service Specification and Its Protocol Specifications in LOTOS—A Survey for Synthesis and Execution," IEICE Trans. on Fundamentals, vol. 75, no. 3, pp. 330-338, 1992.
[8] E. Brinksma, R. Langerak, and P. Broekroelofs, "Functionality Decomposition by Compositional Correctness Preserving Transformation," Computer Aided Verification, CAV'93, 1993.
[9] R. Langerak, "Decomposition of Functionality: A Correctness Preserving LOTOS Transformation," Proc. 10th Int'l IFIP WG 6.1 Symp. Protocol Specification, Testing, and Verification, pp. 203-218, 1991.
[10] H. Mabuchi, K. Takahashi, and N. Shiratori, "Method for Deriving Protocol Specification from Service Definition," Technical Report of IEICE, IN91-110, 1991, in Japanese.
[11] M. Hultstrom, "Structural Decomposition," Proc. 14th Int'l IFIP Symp. Protocol Specification Testing and Verification, pp. 193-209, 1994.
[12] S. Pavon, M. Hultstrom, J. Quemada, D. de Frutos, and Y. Ortega, "Inverse Expansion," Proc. FORTE'91 Fourth Int'l Conf. on: Formal Description Techniques, pp. 303-318, 1991.
[13] E. Brinksma, "Constraint-Oriented Specification in a Constructive Formal Description Technique," Lecture Notes in Computer Science 430, pp. 130-152, 1989.
[14] K. Go and N. Shiratori, "Modularization of a Specification in LOTOS," Proc. Int'l Conf. Network Protocols, pp. 55-62, 1993.
[15] R. Milner, Communication and Concurrency, Prentice-Hall, Englewood Cliffs, N.J., 1989.
[16] ISO, "Information Processing Systems—Open Systems Interconnection—Service Definition for the Association Control Service Element," IS 8649, 1988.
[17] M. van Sindern, L. Ferreira Pires, and C.A. Vissers, "Protocol Design and Implementation Using Formal Methods," The Computer J., vol. 35, no. 5, pp. 478-491, 1992.

Index Terms:
Formal specification, decomposition, LOTOS, constraint-oriented method, equivalence, bisimulation.
Kentaro Go, Norio Shiratori, "A Decomposition of a Formal Specification: An Improved Constraint-Oriented Method," IEEE Transactions on Software Engineering, vol. 25, no. 2, pp. 258-273, March-April 1999, doi:10.1109/32.761449
Usage of this product signifies your acceptance of the Terms of Use.