Abstract
We previously developed a framework, Hydra, for adding formal semantics to a collection of UML diagrams that enable the automated derivation of formal language specifications for those diagrams. Recently, we have also identified a number of requirements patterns for embedded systems that includes sample UML structural and behavioral diagrams for modeling requirements and high-level design for embedded systems. This paper describes a requirements patterns-driven approach for developing UML diagrams for embedded systems, where each pattern has a constraints section to specify safety and other invariant properties. We show how the diagrams for an industrial automotive system, via specifications generated from Hydra, can be automatically analyzed for adherence to these formally specified constraints using the SPIN model checker. We developed the MINERVA framework to support the graphical construction of UML diagrams and to visualize the results from the SPIN analysis in terms of the original UML diagrams.
This work has been supported in part by NSF grants EIA-0000433, EIA-0130724, CDA-9700732, CC-9984726, and CC-9901017, Department of the Navy, Office of Naval Research under Grant No. N00014-01-1-0744, and in cooperation with Siemens Automotive and Detroit Diesel Corporation.
Please contact this author for all correspondences.
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
Ramesh Bharadwaj and Constance L. Heitmeyer. Model checking complete requirements specifications using abstraction. Automated Software Engineering: An International Journal, 6(1):37–68, January 1999.
Grady Booch, James Rumbaugh, and Ivar Jacobson. The Unified Modeling Language User Guide. Addision-Wesley, 1999.
Laura A. Campbell, Betty H. C. Cheng, William E. McUmber, and R. E. K. Stirewalt. Automatically detecting and visualizing errors in UML diagrams. Requirements Engineering Journal, 7(4):264–287, 2002.
Betty H. C. Cheng, Laura A. Campbell, Min Deng, and R. E. K. Stirewalt. Enabling validation of UML formalizations. Technical Report MSU-CSE-02-25, Department of Computer Science, Mich State Univ, E Lansing, MI, September 2002.
Bruce Powell Douglass. Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns. Addison-Wesley, 1999.
Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Property specification patterns for finite-state verification. In Proceedings 2nd Workshop on Formal Methods in Software Engineering, pages 7–16, Clearwater Beach, FL, March 1998.
Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1994.
Wai Ming Ho, Jean-Marc Jezequel, Alain Le Guennec, and Francois Pennaneac’h. UMLAUT: an extendible UML transformation framework. In Proc. of IEEE International Conference on Automated Software Engineering, Cocoa Beach, FL, October 1999.
Gerald J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering, 23(5), May 1997.
Honeywell. URL: http://www.htc.honeywell.com/dome.
I-logix. Rhapsody. URL: http://www.ilogix.com.
Sascha Konrad, Laura A. Campbell, and Betty H. C. Cheng. Adding formal specifications to requirements patterns. In Proceedings of the Requirements for High Assurance Systems Workshop (RHAS02) as part of the IEEE Joint International Conference on Requirements Engineering (RE02), Essen, Germany, September 2002.
Sascha Konrad, Laura A. Campbell, Betty H. C. Cheng, and Min Deng. A requirements pattern-driven approach to specify systems and check properties. Technical Report MSU-CSE-02-28, Computer Science and Engineering, Mich State Univ, E Lansing, MI, December 2002.
Sascha Konrad and Betty H. C. Cheng. Requirements patterns for embedded systems. In Proceedings of the IEEE Joint International Conference on Requirements Engineering (RE02), Essen, Germany, September 2002.
William E. McUmber and Betty H. C. Cheng. A general framework for formalizing UML with formal languages. In Proceedings of IEEE International Conference on Software Engineering (ICSE01), Toronto, Canada, May 2001.
William E. McUmber and Betty H. C. Cheng. UML-based analysis of embedded systems using a mapping to VHDL. In Proceedings of IEEE High Assurance Software Engineering (HASE99), Washington, DC, November 1999.
William Eugene McUmber. A Generic Framework for Formalizing Object-Oriented Modeling Notations for Embedded Systems Development. PhD thesis, Michigan State University, August 2000.
Jorg Niere and Albert Zundorf. Using FUJABA for the development of production control systems. In Applications of Graph Transformations with Industrial Relevance AGTIVE, pages 181–191. Springer Verlag, 1999. Volume 1779, Lecture Notes in Computer Science.
Rational. Rational Rose. URL: http://www.rational.com.
Ian Sommerville. Software Engineering. Addison-Wesley, 1992.
Telelogic. ObjectGEODE. URL: http://www.telelogic.com.
Anthony Torre. Project specifications for diesel filter system, 2000. http://www.cse.msu.edu/~cse470/F2000/cheng/Projects/F00-Cheng/filter/Description/air-filter.html.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Konrad, S., Campbell, L.A., Cheng, B.H.C., Deng, M. (2003). A Requirements Patterns-Driven Approach to Specify Systems and Check Properties. In: Ball, T., Rajamani, S.K. (eds) Model Checking Software. SPIN 2003. Lecture Notes in Computer Science, vol 2648. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44829-2_2
Download citation
DOI: https://doi.org/10.1007/3-540-44829-2_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40117-9
Online ISBN: 978-3-540-44829-7
eBook Packages: Springer Book Archive