Capturing the behavior of a system by use cases have been intensively investigated in the last decade. The challenge is to find both the adequate model that fits the needs of the analyst and a formal composition mechanism which helps the generation of the expected behavior. In this paper, we propose a formal approach for specifying and composing use cases based on assignments. Those assignments are used to express new use cases. An assignment provides the join points and the composition operators that will be taken into account during the composition. These join points are, in fact, determined through a model checking step. They represent states where a property defined by the analyst holds. In order to evaluate these assignments, we define a composition mechanism based on the well known concept of synchronized product.