Advertisement

A Dynamic Assertion-Based Verification Platform for Validation of UML Designs

  • Ansuman Banerjee
  • Sayak Ray
  • Pallab Dasgupta
  • Partha Pratim Chakrabarti
  • S. Ramesh
  • P. Vignesh V. Ganesan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5311)

Abstract

For quite some time, the Unified Modeling Language (UML) [5] has been adopted by designers of safety critical control systems such as automotive and aviation control. This has led to an increased emphasis on setting up a validation flow over UML that can be used to guarantee the correctness of UML models. In this paper, we present a dynamic property verification (DPV) framework for validation of UML designs. The verification engine is built on top of Rhapsody [3], a popular UML simulator, using the concept of dynamic property monitoring over simulation runs. In view of the growing popularity of model-based development, we believe that the verification methodology presented in this paper is of immediate practical value to the UML-based design community.

Keywords

Linear Temporal Logic Event Queue Behavioral Requirement Data Member Assertion Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bhaduri, P., Ramesh, S.: Model Checking of Statechart Models: Survey and Recent Directions (2004)Google Scholar
  2. 2.
    Dasgupta, P.: A Roadmap for Formal Property Verification. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  3. 3.
    Harel, D., Kugler, H.: The Rhapsody semantics of Statecharts (or, On the Executable Core of the UML). In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 325–354. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
  5. 5.
    Object Management Group, Unified Modeling Language Specification, Version 1.4, Draft, OMG(2001), http://cgi.omg.org/cgibin/docad/018214

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Ansuman Banerjee
    • 1
  • Sayak Ray
    • 1
  • Pallab Dasgupta
    • 1
  • Partha Pratim Chakrabarti
    • 1
  • S. Ramesh
    • 2
  • P. Vignesh V. Ganesan
    • 2
  1. 1.Indian Institute of Technology KharagpurIndia
  2. 2.General Motors India Science LabsIndia

Personalised recommendations