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 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 industrial collaborators.
This work has been supported in part by NSF grants EIA-0000433, CNS-0551622, CCF-0541131, IIP-0700329, CCF-0750787, Department of the Navy, Office of Naval Research under Grant No. N00014-01-1-0744, Siemens Corporate Research, and a Quality Fund Program grant from Michigan State University.
We gratefully acknowledge the feedback and insight provided by the reviewers of our earlier work.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Unifed Modeling Language
- Execution Trace
- Latent Behavior
- Unifed Modeling Language Model
- Existence Property
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
McUmber, W.E., Cheng, B.H.C.: A general framework for formalizing UML with formal languages. In: Proceedings of the IEEE International Conference on Software Engineering (ICSE 2001), Toronto, Canada (May 2001)
Lilius, J., Paltor, I.P.: vUML: A tool for verifying UML models. In: Proceedings of the 14th IEEE International Conference on Automated Software Engineering, Washington, DC, USA, p. 255. IEEE Computer Society, Los Alamitos (1999)
Tanuan, M.C.: Automated Analysis of Unifed Modeling Language (UML) Specifications. Master’s thesis, University of Waterloo, Canada (2001)
Uchitel, S., Kramer, J., Magee, J.: Detecting implied scenarios in message sequence chart specifications. SIGSOFT Softw. Eng. Notes 26(5), 74–82 (2001)
Lutz, R.R., Mikulski, I.C.: Requirements discovery during the testing of safety-critical software. In: ICSE 2003: Proceedings of the 25th International Conference on Software Engineering (2003)
Letier, E.: Reasoning about Agents in Goal-Oriented Requirements Engineering. PhD thesis, Louvain-la-Neuve, Belgium (2001)
Acharya, M., Xie, T., Pei, J., Xu, J.: Mining API patterns as partial orders from source code: from usage scenarios to specifications. In: ESEC-FSE 2007, pp. 25–34. ACM, New York (2007)
Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450–463. Springer, Heidelberg (2000)
Chang, R.M., Avrunin, G.S., Clarke, L.A.: Property inference from program executions. Technical Report UM-CS-2006-26, University of Massachusetts (2006)
Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering 27(2), 99–123 (2001)
Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500–517. Springer, Heidelberg (2001)
Gurfinkel, A., Chechik, M., Devereux, B.: Temporal logic query checking: A tool for model exploration. IEEE Transactions on Software Engineering 29(10), 898–914 (2003)
Jeffords, R., Heitmeyer, C.: Automatic generation of state invariants from requirements specifications. SIGSOFT Softw. Eng. Notes 23(6), 56–69 (1998)
Weimer, W., Necula, G.C.: Mining temporal specifications for error detection. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 461–476. Springer, Heidelberg (2005)
Yang, J., Evans, D., Bhardwaj, D., Bhat, T., Das, M.: Perracotta: mining temporal API rules from imperfect traces. In: ICSE 2006: Proceedings of the 28th International Conference on Software Engineering, pp. 282–291. ACM, New York (2006)
Koza, J.R., Keane, M.A., Streeter, M.J., Mydlowec, M., Yu, J., Lanza, G.: Genetic Programming IV: Routine Human-Competitive Machine Intelligence. Springer, Heidelberg (2003)
Lehman, J., Stanley, K.: Exploiting open-endedness to solve problems through the search for novelty. In: Bullock, S., Noble, J., Watson, R., Bedau, M.A. (eds.) Artificial Life XI: Proceedings of the Eleventh International Conference on the Simulation and Synthesis of Living Systems, pp. 329–336. MIT Press, Cambridge (2008)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, pp. 411–420 (1999)
Holzmann, G.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2004)
Konrad, S., Cheng, B.H.C.: Real-time specification patterns. In: Proceedings of the International Conference on Software Engineering (ICSE 2005), St. Louis, MO, USA (May 2005)
Kim, M., Kim, S., Park, S., Choi, M.T., Kim, M., Gomaa, H.: UML-based service robot software development: a case study. In: ICSE 2006: Proceeding of the 28th International Conference on Software Engineering, pp. 534–543 (2006)
Goldsby, H.J., Cheng, B.H.C., McKinley, P.K., Knoester, D.B., Ofria, C.A.: Digital evolution of behavioral models for autonomic systems. In: Proceedings of the 5th International Conference on Autonomic Computing (ICAC 2008), Chicago, Illinois (June 2008)
Smith, R.L., Avrunin, G.S., Clarke, L.A., Osterweil, L.J.: Propel: an approach supporting property elucidation. In: ICSE 2002: Proceedings of the 24th International Conference on Software Engineering, pp. 11–21. ACM, New York (2002)
Cohen, M.B., Dwyer, M.B., Shi, J.: Coverage and adequacy in software product line testing. In: ROSATEA 2006: Proceedings of the ISSTA 2006 Workshop on Role of Software Architecture for Testing and Analysis, pp. 53–63. ACM, New York (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goldsby, H.J., Cheng, B.H.C. (2010). Automatically Discovering Properties That Specify the Latent Behavior of UML Models . In: Petriu, D.C., Rouquette, N., Haugen, Ø. (eds) Model Driven Engineering Languages and Systems. MODELS 2010. Lecture Notes in Computer Science, vol 6394. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16145-2_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-16145-2_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16144-5
Online ISBN: 978-3-642-16145-2
eBook Packages: Computer ScienceComputer Science (R0)