Software benchmarks are essential in evaluating computer science technologies in an objective and fair manner. Whereas this is true for formal software verification, traditional benchmarks prioritize practicality and tend to be the instances of the specific well-known classes of verification problems. The aim of this paper is to provide researchers with benchmarks for evaluating general applicability of software verification technologies such as model checking. We propose a novel benchmark generation method that focuses on model checking for safety properties. The proposed method generates concurrent component processes whose composite systems contain errors. Owing to the complex concurrent behavior, our method enables researchers to apply hard benchmarks to formal error detection of software systems. One of the main technical breakthroughs is to represent an error as a state transition model and embed the error into the given software specification using a model composition technique. Then, a random model decomposition is applied to generate processes. We report our prototype implementation of the proposed method whose implementation language is Python 3 in order to apply the prototype to recent search-based model checking techniques.