Sciweavers

Share
MODELS
2010
Springer

Automatically Discovering Properties That Specify the Latent Behavior of UML Models

9 years 27 days ago
Automatically Discovering Properties That Specify the Latent Behavior of UML Models
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 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 discover a set of properties that cover different regions of the model state space. The Marple-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 Marple 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 indust...
Heather Goldsby, Betty H. C. Cheng
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where MODELS
Authors Heather Goldsby, Betty H. C. Cheng
Comments (0)
books