The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - March/April (1999 vol.25)
pp: 258-273
ABSTRACT
<p><b>Abstract</b>—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.</p>
INDEX TERMS
Formal specification, decomposition, LOTOS, constraint-oriented method, equivalence, bisimulation.
CITATION
Kentaro Go, "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
22 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool