Statistical software testing promises to offer a solution to the growing testing burden caused by the ever-increasing complexity of today's software systems. Nevertheless, the complexity of these systems makes it more difficult to provide a model to use as a basis for statistical testing. The flat and hierarchical modeling currently used to create operational profiles leads to enormous models when capturing the usage of these complex systems. This research describes a method to extend formal specification languages, intended for modeling complex systems, with statistical testing components. With this new procedure for defining operational profiles, we can generate statistical test cases from significantly larger models. This sets the stage for conducting future studies comparing statistical testing to other test strategies, such as structural testing.