Prototyping is an effective and efficient way of requirements validation to avoid introducing errors in the early stage of software development. However, manually developing a prototype of a software system requires additional efforts, which would increase the overall cost of software development. In this article, we present an approach with a developed tool RM2PT to automated prototype generation from formal requirements models for requirements validation. A requirements model consists of a use case diagram, a conceptual class diagram, use case definitions specified by system sequence diagrams, and the contracts of their system operations. A system operation contract is formally specified by a pair of pre and postconditions in object constraint language. We propose a method with a set of transformation rules to decompose a contract into executable parts and nonexecutable parts. An executable part can be automatically transformed into a sequence of primitive operations by applying their corresponding rules, and a nonexecutable part is not transformable with the rules. The tool RM2PT provides a mechanism for developers to develop a piece of program for each nonexecutable part manually, which can be plugged into the generated prototype source code automatically. We have conducted four case studies with over 50 use cases. The experimental result shows that the 93.65% system operations are executable, and only 6.35% are nonexecutable, which can be implemented by developers manually or invoking the third-party application programming interface (APIs). Overall, the result is satisfactory. Each 1 s generated prototype of four case studies requires approximate one day's manual implementation by a skilled programmer. The proposed approach with the developed computer-aided software engineering tool can be applied to the software industry for requirements engineering.