Issue No. 02 - March/April (1999 vol. 25)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.761449
<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>
Formal specification, decomposition, LOTOS, constraint-oriented method, equivalence, bisimulation.
Norio Shiratori, Kentaro Go, "A Decomposition of a Formal Specification: An Improved Constraint-Oriented Method", IEEE Transactions on Software Engineering, vol. 25, no. , pp. 258-273, March/April 1999, doi:10.1109/32.761449