Skip to main content
SpringerLink
Log in

Mapping USE Specifications into Spec#

  • Conference paper
  • First Online:
Software Technologies: Applications and Foundations (STAF 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10748))

Abstract

The UML model is easy to describe the object oriented program components clearly in graphical notation. OCL allows users to express textual constraints about the UML model. The USE tool allows specification to be expressed in a textual format for all features of the UML model with OCL constraints. Spec# is a formal language, which extends C# with constructs for non-null types, preconditions, post conditions, and object invariants. It allows programmers to document their design decisions in the code. Spec# has run time verifier to verify the specification constraints over the C# code. This paper describes the mapping of USE specifications into Spec# which helps to improve the quality of both UML/OCL and Spec#.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Clarke, D., Östlund, J., Sergey, I., Wrigstad, T.: Ownership types: a survey. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. Types, Analysis and Verification. LNCS, vol. 7850, pp. 15–58. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36946-9_3. ISBN 978-3-642-36946-9

    Chapter  Google Scholar 

  2. Hilken, F., Niemann, P., Gogolla, M., Wille, R.: From UML/OCL to base models: transformation concepts for generic validation and verification. In: Kolovos, D., Wimmer, M. (eds.) ICMT 2015. LNCS, vol. 9152, pp. 149–165. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21155-8_12

    Chapter  Google Scholar 

  3. Shimba, H., Hanada, K., Okano, K., Kusumoto, S.: Bidirectional translation between OCL and JML for round-trip engineering. In: 20th Asia-Pacific Software Engineering Conference (APSEC 2013), pp. 49–54. IEEE (2013)

    Google Scholar 

  4. Thangaraj, J., SenthilKumaran, U.: Introducing ownership type constraints to UML/OCL. In: International Workshop on Aliasing, Capabilities and Ownership, IWACO17 co located with the 31st European Conference on Object-Oriented Programming, ECOOP 2017, Barcelona, Spain, June 2017

    Google Scholar 

  5. Leino, K.R.M., Müller, P.: Using the Spec# language, methodology, and tools to write bug-free programs. In: Müller, P. (ed.) LASER 2007-2008. LNCS, vol. 6029, pp. 91–139. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-13010-6_4

    Chapter  Google Scholar 

  6. Gogolla, M., Buttner, F., Richters, M.: USE: a UML-based specification environment for validating UML and OCL. Sci. Comput. Program. 69, 27–34 (2007). Elseveir

    Article  MathSciNet  MATH  Google Scholar 

  7. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30569-9_3. ISBN 978-3-540-30569-9

    Chapter  Google Scholar 

  8. OMG: Object Constraint Language (OCL): Version 2.3.1., Object Management Group (2012). http://www.omg.org/spec/OCL/2.3.1

  9. OMG: Unified Modeling Language (UML): Version 2.4.1., Object Management Group (2011). http://www.omg.org/spec/UML/2.4.1

  10. Monahan, R., Leino, K.R.M.: Program verification using the Spec# programming system. In: ECOOP Tutorial (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Information Technology and Engineering, VIT University, Vellore, TN, India

    Jagadeeswaran Thangaraj & SenthilKumaran Ulaganathan

Authors
  1. Jagadeeswaran Thangaraj
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. SenthilKumaran Ulaganathan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jagadeeswaran Thangaraj .

Editor information

Editors and Affiliations

  1. Johannes Kepler University of Linz, Linz, Austria

    Martina Seidl

  2. Department of Informatics, King’s College London, London, United Kingdom

    Steffen Zschaler

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Thangaraj, J., Ulaganathan, S. (2018). Mapping USE Specifications into Spec#. In: Seidl, M., Zschaler, S. (eds) Software Technologies: Applications and Foundations. STAF 2017. Lecture Notes in Computer Science(), vol 10748. Springer, Cham. https://doi.org/10.1007/978-3-319-74730-9_29

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-74730-9_29

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-74729-3

  • Online ISBN: 978-3-319-74730-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation