Automatically Discovering Properties that Specify the Latent Behavior of UML Models

Abstract

Abstract. 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 tem-poral logic properties that specify the latent 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 Marple, a evolutionary-computation tool that leverages natural selection to dis-cover a set of properties that cover different regions of the model state space. TheMarple-discovered properties can be used to refine the mod-els to either remove unwanted behavior or to explicitly document a desir-able property as required system behavior. We use Marple to discover unwanted latent behavior in two applications: an autonomous robot nav-igation system and an automotive door locking control system obtained from one of our industrial collaborators. 1