Abstract
SysML activity diagrams are OMG/INCOSE standard models for specifying and analyzing systems’ behaviors. In this paper, we propose an abstraction approach for this type of diagrams that helps to mitigate the state-explosion problem in probabilistic model checking. To this end, we present two algorithms to reduce the size of a given SysML activity diagram. The first eliminates the irrelevant behaviors regarding the property under check, while the second merges control nodes into equivalent ones. The resulting abstracted model can answer safely the Probabilistic Computation Tree Logic (PCTL) property. Moreover, we present a novel calculus for activity diagrams (NuAC) that captures their underlying semantics. In addition, we prove the soundness of our approach by defining a probabilistic weak simulation relation between the semantics of the abstract and the concrete models. This relation is shown to preserve the satisfaction of the PCTL properties. Finally, we demonstrate the effectiveness of our approach on an online shopping system case study.
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
Debbabi, M., Hassane, F., Jarraya, Y., Soeanu, A., Alawneh, L.: Verification and Validation in Systems Engineering - Assessing UML / SysML Design Models. Springer (2010)
Ouchani, S., Jarraya, Y., Mohamed, O.A.: Model-based systems security quantification. In: PST, pp. 142–149 (2011)
Baier, C., Katoen, J.P.: Principles of Model Checking, MIT Press (May 2008)
Xin-feng, Z., Jian-dong, W., Xin-feng, Z., Bin, L., Jun-wu, Z., Jun, W.: Methods to tackle state explosion problem in model checking. In: Proceedings of the 3rd Int. Conf. on IITA, pp. 329–331. IEEE Press, NJ (2009)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification. Springer (2001)
OMG, OMG Systems Modeling Language (OMG SysML) Specification, Object Management Group, OMG Available Specification (September 2007)
Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated Verification Techniques for Probabilistic Systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011)
P. Team. PRISM - Probabilistic Symbolic Model Checker, http://www.prismmodelchecker.org (last visited November 2011)
Ober, I., Graf, S., Ober, I.: Model Checking of UML Models via a Mapping to Communicating Extended Timed Automata. In: SPIN 2004. LNCS, vol. 2989 (2004)
Ober, I., Graf, S., Ober, I.: Validating Timed UML models by simulation and verification. In: Workshop SVERTS, San Francisco (October 2003)
Westphal, B.: LSC Verification for UML Models with Unbounded Creation and Destruction. Electronic Notes in Theoretical Computer Science 144, 133–145 (2006)
Prashanth, C.M., Shet, K.C.: Efficient Algorithms for Verification of UML Statechart Models. Journal of Software 4, 175–182 (2009)
Daoxi, C., Guangquan, Z., Jianxi, F.: Abstraction framework and complexity of model checking based on the Promela models. In: 4th International Conference on Computer Science Education, ICCSE 2009, pp. 857–861 (July 2009)
Xie, F., Browne, J.C.: Integrated State Space Reduction for Model Checking Executable Object-Oriented Software System Designs. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 64–79. Springer, Heidelberg (2002)
Xie, F., Levin, V., Browne, J.C.: ObjectCheck: A Model Checking Tool for Executable Object-Oriented Software System Designs. In: Fundamental Approaches to Software Engineering, pp. 331–335 (2002)
ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A State/Event-Based Model-Checking Approach for the Analysis of Abstract System Properties. Sci. Comput. Program. 76, 119–135 (2011)
Yang, H.: Abstracting UML Behavior Diagrams for Verification. In: Software Evolution With Uml And Xml, pp. 296–320. IGI Publishing, Hershey (2005)
Eshuis, R.: Symbolic Model Checking of UML Activity Diagrams. ACM Transactions on Software Engineering and Methodology 15 (2006)
Eshuis, R., Wieringa, R.: Tool support for verifying uml activity diagrams. IEEE Transactions on Software Engineering 30 (2004)
Holt, J., Perry, S.: SysML for Systems Engineering. Institution of Engineering and Technology Press (January 2007)
OMG, OMG Unified Modeling Language: Superstructure 2.1.2, Object Management Group (November 2007)
Segala, R.: A Compositional Trace-Based Semantics for Probabilistic Automata. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 234–248. Springer, Heidelberg (1995)
Milner, R.: Communicating and mobile systems - the Pi-calculus. Cambridge University Press (1999)
Gomaa, H.: Software Modeling and Design: UML, Use Cases, Patterns, and Software Architectures. Cambridge University Press (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ouchani, S., Ait Mohamed, O., Debbabi, M. (2012). Efficient Probabilistic Abstraction for SysML Activity Diagrams. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds) Software Engineering and Formal Methods. SEFM 2012. Lecture Notes in Computer Science, vol 7504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33826-7_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-33826-7_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33825-0
Online ISBN: 978-3-642-33826-7
eBook Packages: Computer ScienceComputer Science (R0)