Abstract
Increasingly, object-oriented technology, specifically the Unified Modeling Language (UML), is being used to develop critical embedded systems. Several efforts have attempted to translate UML models into formal specification languages, thus enabling the models to be analyzed by model checkers. Unfortunately, the complexity and volume of the analysis results often prevents developers from fully taking advantage of the analysis capabilities. This paper introduces a generic visualization framework, Theseus, that provides developers with a model-based, visual interpretation of the analysis results in terms of the original UML diagrams. Within this framework, a playback mechanism displays the execution path that has led to a model checking violation in terms of the original UML state diagram and a newly generated sequence diagram that depicts the problem scenario. A Theseus prototype supporting the Spin and SMV model checkers has been applied to the analysis of UML models for embedded systems from industry.
This work has been supported in part by NSF grants EIA-0000433, EIA-0130724, CDA-9700732, CCR-9901017, CNS-0551622, CCF-0541131, Department of the Navy, Office of Naval Research under Grant No. N00014-01-1-0744, Eaton Corporation, Siemens Corporate Research, and a grant from Michigan State University’s Quality Fund. Stephane Kamdoum completed a portion of this work while studying under an International Exchange Program between the University of Kaiserslautern and Michigan State University.
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
Douglass, B.P.: Real-Time Design Patterns. Addison-Wesley, Reading (2003)
Object Management Group, http://www.omg.org
McUmber, W.E., Cheng, B.H.C.: A general framework for formalizing UML with formal languages. In: Proc. of the IEEE Int. Conf. on Software Engineering (ICSE 2001), Toronto, Canada (2001)
Lilius, J., Paltor, I.P.: vUML: A tool for verifying UML models. In: Proc. of the 14th IEEE Int. Conf. on Automated Software Engineering, Washington (1999)
Tanuan, M.C.: Automated Analysis of Unifed Modeling Language (UML) Specifications. Master’s thesis, University of Waterloo, Canada (2001)
Inverardi, P., Muccini, H., Pelliccione, P.: CHARMY: An Extensible Tool for Architectural Analysis. In: ESEC/FSE-13: Proc. of the 10th European Software Engineering Conf. held jointly with 13th ACM SIGSOFT Int. Symposium on Foundations of Software Engineering (2005)
Holzmann, G.: The Spin Model Checker (2003)
McMillan, K.L.: Getting started with SMV (1999)
IBM: Rational Rose XDE Developer (2005), http://www-306.ibm.com/software/awdtools/developer/rosexde/
Telelogic: ObjectGEODE (2005), http://www.telelogic.com/
I-logix (2005), http://www.ilogix.com/
ARTiSAN Software: Real-time Studio (2005), http://www.artisansw.com
Ho, W.M., Jézéquel, J.M., Guennec, A.L., Pennaneac, F.: UMLAUT: an extendible UML transformation framework. In: Proc. of the Automated Software Engineering Conf., Florida (1999)
Nickel, U., Niere, J., Zündorf, A.: The FUJABA environment. In: Proc. of the 22nd Int. Conf. on Software Engineering, pp. 742–745. ACM Press, New York (2000)
Konrad, S., Cheng, B.H.C., Campbell, L.A.: Object Analysis Patterns for Embedded Systems. IEEE Trans. on Software Engineering 30(12), 970–992 (2004)
Konrad, S., Cheng, B.H.C.: Facilitating the construction of specification pattern-based properties. In: Proc. of the IEEE Int. Requirements Engineering Conf (RE 2005), Paris, France (2005)
Konrad, S., Cheng, B.H.C.: Automated analysis of natural language properties for UML models. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol. 3844, pp. 48–57. Springer, Heidelberg (2006)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer, New York (1992)
Tigris.org: ArgoUML: The project home (2005), http://argouml.tigris.org
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1994)
Konrad, S., Cheng, B.H.C.: Real-time specification patterns. In: Proc. of the Int. Conf. on Software Engineering (ICSE 2005), St Louis, MO, USA (2005)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proc. of the 21st Int. Conf. on Software Engineering, pp. 411–420. IEEE Computer Society Press, Los Alamitos (1999)
McMillan, K.L.: Symbolic Model Checking. PhD thesis, Carnegie Mellon University (1993)
Kamdoum, S.: Facilitating the roundtrip engineering of model-driven software architecture. Master’s thesis, Michigan State University (2006)
Pettersson, P., Larsen, K.G.: Uppaal2k. Bulletin of the European Association for Theoretical Computer Science 70, 40–44 (2000)
Mikk, E., Lakhnech, Y., Siegel, M., Holzmann, G.J.: Implementing statecharts in promela/spin. In: WIFT 1998: Proc. of the Second IEEE Workshop on Industrial Strength Formal Specification Techniques, p. 90 (1998)
Crane, M.L., Dingel, J.: UML vs. classical vs. Rhapsody statecharts: Not all models are created equal. In: Proc. of the ACM/IEEE 8th Int. Conf. on Model Driven Engineering Languages and Systems (2005)
Knapp, A., Merz, S., Rauh, C.: Model checking timed UML state machines and collaborations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 395–414. Springer, Heidelberg (2002)
Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a model-checking tool for real-time systems. In: Proc. of the 10th Conference on Computer-Aided Verification (1998)
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
Goldsby, H., Cheng, B.H.C., Konrad, S., Kamdoum, S. (2006). A Visualization Framework for the Modeling and Formal Analysis of High Assurance Systems. 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_49
Download citation
DOI: https://doi.org/10.1007/11880240_49
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)