This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A UML/MARTE Model Analysis Method for Uncovering Scenarios Leading to Starvation and Deadlocks in Concurrent Systems
March-April 2012 (vol. 38 no. 2)
pp. 354-374
ASCII Text
x 
 
Marwa Shousha, Lionel C. Briand, Yvan Labiche, "A UML/MARTE Model Analysis Method for Uncovering Scenarios Leading to Starvation and Deadlocks in Concurrent Systems," IEEE Transactions on Software Engineering, vol. 38, no. 2, pp. 354-374, March-April, 2012.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2010.107,
author = {Marwa Shousha and Lionel C. Briand and Yvan Labiche},
title = {A UML/MARTE Model Analysis Method for Uncovering Scenarios Leading to Starvation and Deadlocks in Concurrent Systems},
journal ={IEEE Transactions on Software Engineering},
volume = {38},
number = {2},
issn = {0098-5589},
year = {2012},
pages = {354-374},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2010.107},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - A UML/MARTE Model Analysis Method for Uncovering Scenarios Leading to Starvation and Deadlocks in Concurrent Systems
IS - 2
SN - 0098-5589
SP354
EP374
EPD - 354-374
A1 - Marwa Shousha,
A1 - Lionel C. Briand,
A1 - Yvan Labiche,
PY - 2012
KW - Search-based software engineering
KW - MDD
KW - deadlock
KW - starvation
KW - model analysis
KW - concurrent systems
KW - UML
KW - MARTE
KW - genetic algorithms.
VL - 38
JA - IEEE Transactions on Software Engineering
ER -
 
Marwa Shousha, Carleton University, Ottawa
Lionel C. Briand, Simula Research Laboratory, Lysaker and University of Oslo, Norway
Yvan Labiche, Carleton University, Ottawa
Concurrency problems such as starvation and deadlocks should be identified early in the design process. As larger, more complex concurrent systems are being developed, this is made increasingly difficult. We propose here a general approach based on the analysis of specialized design models expressed in the Unified Modeling Language (UML) that uses a specifically designed genetic algorithm to detect concurrency problems. Though the current paper addresses deadlocks and starvation, we will show how the approach can be easily tailored to other concurrency issues. Our main motivations are 1) to devise solutions that are applicable in the context of the UML design of concurrent systems without requiring additional modeling and 2) to use a search technique to achieve scalable automation in terms of concurrency problem detection. To achieve the first objective, we show how all relevant concurrency information is extracted from systems' UML models that comply with the UML Modeling and Analysis of Real-Time and Embedded Systems (MARTE) profile. For the second objective, a tailored genetic algorithm is used to search for execution sequences exhibiting deadlock or starvation problems. Scalability in terms of problem detection is achieved by showing that the detection rates of our approach are, in general, high and are not strongly affected by large increases in the size of complex search spaces.

[1] M. Abadi, C. Flanagan, and S.N. Freund, "Types for Safe Locking: Static Race Detection for Java," ACM Trans. Programming Languages and Systems, vol. 28, no. 2, pp. 207-255, 2006.
[2] O. Abdellatif-Kaddour, P. Thevenod-Fosse, and H. Waeselynck, "Property-Oriented Testing Based on Simulated Annealing," http://www.laas.fr/~francois/SVF/seminaires/ inputs/02 olfapaper.pdf, 2001.
[3] W. Afzal, R. Torkar, and R. Feldt, "A Systematic Mapping Study on Non-Functional Search-Based Software Testing," Information and Software Technology, vol. 51, no. 6, pp. 957-976, 2009.
[4] E. Alba and F. Chicano, "Finding Safety Errors with ACO," Proc. Genetic and Evolutionary Computation Conf., pp. 1066-1073, 2007.
[5] S. Ali, L.C. Briand, H. Hemmati, and R.K. Panesar-Walawege, "A Systematic Review of the Application and Empirical Investigation of Search-Based Test-Case Generation," IEEE Trans. Software Eng, vol. 35, no. 6, pp. 742-762, Nov./Dec. 2009.
[6] T. Back, "Self-Adaptation in Genetic Algorithms," Proc. European Conf. Artificial Life, pp. 263-271, 1992.
[7] J. Bacon, Concurrent Systems—Operating Systems, Database and Distributed Systems: An Integrated Approach, second ed., Addison-Wesley, 1997.
[8] G. Behrmann, A. David, and K.G. Larsen, "A Tutorial on Uppaal," http://www.it.uu.se/research/group/darts/ papers/texts new-tutorial.pdf, 2004.
[9] G. Brat, K. Havelund, S. Park, and W. Visser, "Java Pathfinder Second Generation of a Java Model Checker," Proc. Workshop Advances in Verification, 2000.
[10] R. Chugh, J.W. Voung, R. Jhala, and S. Lerner, "Dataflow Analysis for Concurrent Programs Using Datarace Detection," Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 316-326, 2008.
[11] S. Demathieu, F. Thomas, C. Andre, S. Gerard, and F. Terrier, "First Experiments Using the UML Profile for MARTE," Proc. 11th IEEE Symp. Object Oriented Real-Time Distributed Computing, pp. 50-57, 2008.
[12] M. Dorigo and V. Maniezzo, "Parallel Genetic Algorithms: Introduction and Overview of Current Research," Parallel Genetic Algorithms: Theory and Applications, J. Stender, ed., pp. 5-43, IOS Press, 1993.
[13] A.B. Downey, The Little Book of Semaphores, second ed. Green Tea Press, 2008.
[14] S. Edelkamp, A. Lluch-Lafuente, and S. Leue, "Trail-Directed Model Checking," Electronic Notes in Theoretical Computer Science, vol. 55, no. 3, pp. 343-356, Oct. 2001.
[15] C. Flanagan and S.N. Freund, "Type-Based Race Detection for Java," ACM SIGPLAN Notices, vol 35, no. 5, pp. 219-232, 2000.
[16] C. Flanagan, K. Rustan, M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, and R. Stata, "Extended Static Checker for Java," ACM SIGPLAN Notices, vol. 37, no. 5, pp. 234-245, 2002.
[17] P. Gagnon, F. Mokhati, and M. Badri, "Applying Model Checking to Concurrent UML Models," J. Object Technology, vol. 7, no. 1, pp. 59-84, 2008.
[18] P. Godefroid and S. Khurshid, "Exploring Very Large State Spaces Using Genetic Algorithms," Int'l J. Software Tools for Technology Transfer, vol. 6, no. 2, pp. 117-127, Aug. 2004.
[19] H. Gomaa, Designing Concurrent, Distributed, and Real-Time Applications with UML. Addison-Wesley, 2000.
[20] S. Gradara, A. Sontone, and M.L. Villani, "DELFIN+: An Efficient Deadlock Detection Tool for CCS Processes," J. Computer and System Sciences, vol. 72, no. 8, pp. 1397-1412, Apr. 2006.
[21] M. Harman, "The Current State and Future of Search Based Software Engineering," Proc. Int'l Conf Software Eng., pp. 342-357, 2007.
[22] R.L. Haupt and S.E. Haupt, Practical Genetic Algorithms. Wiley-Interscience, 1998.
[23] G.J. Holzmann, "The Model Checker SPIN," IEEE Trans. Software Eng., vol. 23, no. 5, pp. 279-295, May 1997.
[24] C. Jacob, Illustrating Evolutionary Computation with Mathematica. Morgan Kaufmann, 2001.
[25] V. Kahlon, Y. Yang, S. Sankaranarayanan, and A. Gupta, "Fast and Accurate Static Data-Race Detection for Concurrent Programs," Proc. 19th Int'l Conf. Computer Aided Verification, pp. 226-239, 2007.
[26] S. Kim, L. Wildman, and R. Duke, "A UML Approach to the Generation of Test Sequences for JAVA-Based Concurrent Systems," Proc. Australian Conf. Software Eng., pp. 100-109, 2005.
[27] A. Kleppe, J. Warmer, and W. Bast, MDA Explained—The Model Driven Architecture: Practice and Promise, Addison-Wesley, 2003.
[28] A. Knapp and J. Wuttke, "Model Checking of UML 2.0 Interactions," Proc. Int'l Conf. Models in Software Eng., pp. 42-51, 2007.
[29] J.R. Koza, Genetic Programming: On the Programming of Computers by Means of Natural Selection. MIT Press, 1992.
[30] B. Lei, L. Wang, and X. Li, "UML Activity Diagram Based Testing of Java Concurrent Programs for Data Race and Inconsistency," Proc. First Int'l Conf. Software Testing, Verification and Validation, pp. 200-209, 2008.
[31] C. Mradiha, Y. Tanguy, C. Jouvray, F. Terrier, and S. Gerard, "An Execution Framework for MARTE-Based Models," Proc. 13th IEEE Int'l Conf. Eng. of Complex Computer Systems, pp. 222-227, 2008.
[32] S. Oaks and H. Wong, Java Threads, third ed., O'Reilly Media Inc., 2004.
[33] OMG, UML Profile for Modeling and Analysis of Real-Time and Embedded Systems, version 1.0, http://www.omg.org/spec/MARTE/1.0PDF, 2009.
[34] OMG, UML Profile for Schedulability, Performance and Time Specification, http://www.omg.org/docs/formal05-01-02.pdf . 2005.
[35] OMG, Unified Modeling Language (UML), version 2.2, http://www.omg.org/spec/UML/2.2/Superstructure PDF/, 2009.
[36] G. Palshikar, "An Introduction to Model Checking," Embedded Systems Design, http://www.embedded.com/columns/ technicalinsights 17603352?_requestid=68213 , 2004.
[37] D.C. Petriu, "Performance Analysis with the SPT Profile," Model-Driven Eng. for Distributed and Embedded Systems, pp. 205-224, Hermes Science Publishing Ltd., 2005.
[38] A. Rosete-Suárez, A. Ochoa-Rodríguez, and M. Sebag, "Automatic Graph Drawing and Stochastic Hill Climbing," Proc. Genetic and Evolutionary Computation Conf., vol. 2, pp. 1699-1706, 1999.
[39] M. Safe, J. Carballido, I. Ponzoni, and N. Brignole, "On Stopping Criteria for Genetic Algorithms," Proc. 17th Brazilian Symp. Artificial Intelligence, pp. 405-413, 2004.
[40] S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson, "Eraser: A Dynamic Data Race Detector for Multithreaded Programs," ACM Trans. Computer Systems, vol. 15, no. 4, pp. 391-411, 1997.
[41] F. Schneider, "UML and Model Checking," Proc. Fifth Langley Formal Methods Workshop, 1999.
[42] M. Shousha, L. Briand, and Y. Labiche, "A UML/SPT Model Analysis Methodology for Concurrent Systems Based on Genetic Algorithms," Proc. ACM/IEEE Int'l Conf. Model Driven Eng. Languages and Systems, pp. 475-489, 2008.
[43] R. Sinclair, Codenotes for Java: Intermediate and Advanced Language Features, G. Bill, ed. Random House, 2002.
[44] N. Tracey, J. Clark, J. McDermid, and K. Mander, "Integrating Safety Analysis with Automatic Test-Data Generation for Software Safety Verification," Proc. 17th Int'l System Safety Conf., pp. 128-137, 1999.
[45] L. Wang et al., "A Comparative Study of Five Parallel Genetic Algorithms Using the Traveling Salesman Problem," Proc. 12th Int'l Parallel Processing Symp., pp. 345-349, 1998.
[46] H. Yang, "Deadlock," Java Tutorials—Herong's Tutorial Notes, version 4.10, http://www.herongyang.com/javaindex.html , 2006.

Index Terms:
Search-based software engineering, MDD, deadlock, starvation, model analysis, concurrent systems, UML, MARTE, genetic algorithms.
Citation:
Marwa Shousha, Lionel C. Briand, Yvan Labiche, "A UML/MARTE Model Analysis Method for Uncovering Scenarios Leading to Starvation and Deadlocks in Concurrent Systems," IEEE Transactions on Software Engineering, vol. 38, no. 2, pp. 354-374, March-April 2012, doi:10.1109/TSE.2010.107
Usage of this product signifies your acceptance of the Terms of Use.