Abstract
This paper describes methods and tools for automated safety analysis of UML statechart specifications. The general safety criteria described in the literature are reviewed and automated analysis techniques are proposed. The techniques based on OCL expressions and graph transformations are detailed and their limitations are discussed. To speed up the checker methods, a reduced form for UML statecharts is introduced. Using this form, the correctness and completeness of some checker methods can be proven. An example illustrates the application of the tools developed so far.
Supported by the Hungarian Scientific Research Fund under contract OTKA-F030553.
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
Object Management Group: Unified Modeling Language Specification v 1.3. (1999).
B. P. Douglass: Real-Time UML-Developing Efficient Objects for Embedded Systems. Addison-Wesley (1998)
N. G. Leveson: Safeware: System Safety and Computers. Addison-Wesley (1995)
N. G. Leveson, M. P. E. Heimdahl, H. Hildreth, and J. D. Reese: Requirements Specification for Process-Control Systems. IEEE Trans. on SE, pp. 684–706 (1994)
M. P. E. Heimdahl and N. G. Leveson: Completeness and Consistency Checking of Software Requirements. IEEE Trans, on Software Engineering, Vol. 22. No. 6 (1996)
N. G. Leveson, J. D. Reese and M. Heimdahl: SpecTRM: A CAD System for Digital Automation. Digital Avionics System Conference, Seattle (1998)
N. G. Leveson, M. P. E. Heimdahl, and J. D. Reese: Designing Specification Languages for Process Control Systems. Lessons Learned and Steps to the Future.
D. Latella, I. Majzik, M. Massink: Automatic Verification of a Behavioral Subset of UML Statechart Diagrams Using the SPIN Model-checker. Formal Aspects of Computing, Vol. 11 No. 6 pp 637–664, Springer Verlag, (1999)
Rational Corporation. Rational Rose 2000. http://www.rational.com/
G. Holzmann: The Model Checker SPIN. IEEE Transactions on Software Engineering, Vol. 23, pp 279–295 (1997)
M. Gogolla, F. Parisi Presicce: State Diagrams in UML: A Formal Semantics using Graph Transformation. Proc. ICSE’98 Workshop on Precise Semantics of Modeling Techniques (PSMT’98), pp 55–72. (1998)
M. Gogolla: Graph Transformation on the UML Metamodel, Workshop on Graph Transformation and Visual Modeling Techniques, ICALP’2000, Geneva, Switzerland, 2000
Zs. Pap, I. Majzik, A. Pataricza and A. Szegi: Completeness and Consistency Analysis of UML Statechart Specifications. Accepted to DDECS-2001, Gy•r, Hungary (2001)
D. Varró, G. Varró, and A. Pataricza: Automatic Graph Transformation in System Verification. In Proc. DDECS-2000, pp 34, 2000.
Object Management Group. XML Metadata Interchange. (1998).
Zs. Pap: Checking Safety Criteria in UML Statecharts (In Hungarian). Technical Report No. 2/2001 of the DMIS, Budapest University of Technology and Economics, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pap, Z., Majzik, I., Pataricza, A. (2001). Checking General Safety Criteria on UML Statecharts. In: Voges, U. (eds) Computer Safety, Reliability and Security. SAFECOMP 2001. Lecture Notes in Computer Science, vol 2187. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45416-0_5
Download citation
DOI: https://doi.org/10.1007/3-540-45416-0_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42607-3
Online ISBN: 978-3-540-45416-8
eBook Packages: Springer Book Archive