What does it mean to compose two systems? TLA+ models an execution of a system as a sequence of atomic actions. When systems are modeled in this way, the only general definition of the composition of two systems I know if is that it is a system whose executions are sequences of atomic actions, each of which is an action of one of the two systems.
Let Next1 and Next2 be the next-state relations of the two systems. If both systems are described with the same collection of variables then this definition of composition means that their composition has the next-state relation Next1 \/ Next2. If each has private variables that don't appear in the other spec, as well as variables that appear in both, then one usually defines composition to mean that actions of one of the systems leaves unchanged the private variables of the other. Their composition then has the next-state relation
\/ Next1 /\ UNCHANGED pvars1
\/ Next2 /\ UNCHANGED pvars2
where pvars1 and pvars2 are the tuples of private variables of the two systems.
Ioannis asks the right questions about why you are decomposing the specification. I will point out that re-use of specifications should not be a concern. Specifications are short enough that cut-and-paste is a perfectly satisfactory method of re-using a spec. Re-use of the implementation of a specification may be important. This means that you would like to write a specification of a component, and be able to verify the correctness of a system that uses the component looking only at the component's specification. That problem is what the "Conjoining Specifications" paper is about.
Leslie