Abstract
This work describes a new approach for behaviour model extraction which combines static and dynamic information. We exploit context information as a way of merging these types of information. Contexts are defined by evaluated control predicates and values of attributes. They create a nested structure that can facilitate the extraction of causal relations between system actions. We show how context information can guide the process of constructing LTS models that are good approximations of the actual behaviour of the systems they describe. These models can be used for automated analysis and property verification. Augmentation of the values of attributes recorded in contexts produces further refined models and leads towards correct models. Completeness of the extracted models depends on the coverage achieved by samples of executions. Our approach is partially automated by a tool called LTSE. Results of one of our case studies are presented and discussed.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aho, A., Sethi, R., Ullman, J.: Compilers: Principles, Techniques and Tools. Addison-Wesley, Reading (1986)
Ball, T., Rajamani, S.K.: The SLAM Project: Debugging System Software via Static Analysis. In: POPL 2002, Portland, OR, USA, pp. 1–3 (2002)
Boroday, S., Petrenko, A., Singh, J., et al.: Dynamic Analysis of Java Applications for Multithreaded Antipatterns. In: WODA 2005, pp. 1–7 (2005)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Cook, J.E., Wolf, A.L.: Discovering Models of Software Processes from Event-Based Data. ACM TOSEM 7(3), 215–249 (1998)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: Extracting Finite-State Models from Java Source Code. In: ICSE 2000, Limerick, Ireland, pp. 439–448 (2000)
Cordy, J.R., Dean, T.R., Malton, A.J., Schneider, K.A.: Source Transformation in Software Engineering Using the TXL Transformation System. Journal of Information and Software Technology, Special Issue on Source Code Analysis and Manipulation 44(13), 827–837 (2002)
Ernst, M.D.: Static and Dynamic Analysis: Synergy and Duality. In: WODA 2003, Portland, OR, USA, pp. 24–27 (2003)
Godefroid, P.: Software Model Checking: The Verisoft Approach. Bell Labs Technical Memorandum ITD-03-44189G, Bell Laboratories (August 2003)
Havelund, K., Pressburguer, T.: Model Checking Java Programs Using Java PathFinder. Intl. Journal on Software Tools for Technology Transfer 2(4), 366–381 (2000)
Henzinger, T.A., Jahla, R., Majumdar, R., et al.: Lazy Abstraction. In: POPL 2002, pp. 58–70 (2002)
Holzmann, G.J.: From Code to Models. In: ACSD 2001, Newcastle upon Tyne, UK, pp. 3–10 (2001)
Holzmann, G.J., Smith, M.H.: A Practical Method for Verifying Event-Driven Software. In: ICSE 1999, Los Angeles, USA, pp. 597–607 (1999)
Jackson, D., Rinard, M.: Software Analysis: A Roadmap. In: ICSE 2000, Limerick, Ireland, pp. 133–145 (2000)
King, J.C.: Symbolic Execution and Program Testing. CACM 19(7), 385–394 (1976)
Magee, J., Kramer, J.: Concurrency: State Models and Java Programs. Wiley, Chichester (1999)
Mariani, L.: Behavior Capture and Test: Dynamic Analysis of Component-Based Systems. Phd, Università degli Studi di Milano Bicocca (2005)
Milner, R.: An algebraic definition of simulation between programs. In: IJCAI, pp. 481–489 (1971)
Nimmer, J.W., Ernst, M.D.: Automatic Generation of Program Specifications. In: ISSTA 2002, Rome, Italy, pp. 232–242 (2002)
Robschink, T., Snelting, G.: Efficient Path Conditions in Dependence Graphs. In: ICSE 2002, Orlando, Florida, USA, pp. 478–488 (2002)
Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model Checking Programs. Automated Software Engineering Journal 10(2), 203–232 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Duarte, L.M., Kramer, J., Uchitel, S. (2006). Model Extraction Using Context Information. In: Nierstrasz, O., Whittle, J., Harel, D., Reggio, G. (eds) Model Driven Engineering Languages and Systems. MODELS 2006. Lecture Notes in Computer Science, vol 4199. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11880240_27
Download citation
DOI: https://doi.org/10.1007/11880240_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-45772-5
Online ISBN: 978-3-540-45773-2
eBook Packages: Computer ScienceComputer Science (R0)