Formal analysis can be used to verify that a model of the system adheres to its requirements. As such, traditional formal analysis focuses on whether known (desired) system properties are satisfied. In contrast, this paper proposes an automated approach to generating temporal logic properties that specify the
behavior of existing UML models; these are unknown properties exhibited by the system that may or may not be desirable. A key component of our approach is M
, a evolutionary-computation tool that leverages natural selection to discover a set of properties that cover different regions of the model state space. The M
-discovered properties can be used to refine the models to either remove unwanted behavior or to explicitly document a desirable property as required system behavior. We use M
to discover unwanted latent behavior in two applications: an autonomous robot navigation system and an automotive door locking control system obtained from one of our industrial collaborators.