Skip to main content
SpringerLink
Log in
Book cover

International Conference on Software Language Engineering

SLE 2011: Software Language Engineering pp 223–242Cite as

Formalizing a Domain Specific Language Using SOS: An Industrial Case Study

  • Conference paper

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

Abstract

This paper describes the process of formalizing an existing, industrial domain specific language (DSL) that is based on the task-resource paradigm. Initially, the semantics of this DSL is defined informally and implicitly through an interpreter. The formalization starts by projecting the existing concrete syntax onto a formal abstract syntax that defines the language operators and process terms. Next, we define the dynamic operational semantics at the level of individual syntactical notions, using structural operational semantics (SOS) as a formal meta-language. Here, the impact of the formalization process on the DSL is considered in terms of disambiguation of underlying (semantic) language design decisions.

This is a preview of subscription content, 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 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aredo, D.B.: A Framework for Semantics of UML Sequence Diagrams in PVS. Journal of Universal Computer Science 8(7), 674–697 (2002)

    Google Scholar 

  2. Baeten, J.C.M., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories of Communicating Processes (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press (December 2009)

    Google Scholar 

  3. Bol, R.N., Groote, J.F.: The Meaning of Negative Premises in Transition System Specifications. J. ACM 43(5), 863–914 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  4. Börger, E.: High Level System Design and Analysis Using Abstract State Machines. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 1–43. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  5. Börger, E., Cavarra, A., Riccobene, E.: An ASM Semantics for UML Activity Diagrams. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 293–308. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  6. Cabot, J., Clarisó, R., Riera, D.: Verification of UML/OCL Class Diagrams using Constraint Programming. In: ICSTW 2008, pp. 73–80. IEEE Computer Society (2008)

    Google Scholar 

  7. Clark, T., Warmer, J. (eds.): Object Modeling with the OCL. LNCS, vol. 2263. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  8. Combemale, B., Crégut, X., Garoche, P.-L., Thirioux, X.: Essay on Semantics Definition in MDE - An Instrumented Approach for Model Verification. JSW 4(9), 943–958 (2009)

    Article  Google Scholar 

  9. David, A., Möller, M.O., Yi, W.: Formal Verification of UML Statecharts with Real-Time Extensions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 218–232. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Di Ruscio, D., Jouault, F., Kurtev, I., Bézivin, J., Pierantonio, A.: Extending AMMA for Supporting Dynamic Semantics Specifications of DSLs. Technical Report n. 06.02, Laboratoire d’Informatique de Nantes-Atlantique (April 2006)

    Google Scholar 

  11. Evermann, J., Wand, Y.: Toward Formalizing Domain Modeling Semantics in Language Syntax. IEEE Trans. Software Eng. 31(1), 21–37 (2005)

    Article  Google Scholar 

  12. Graaf, B., Weber, S., van Deursen, A.: Model-Driven Migration of Supervisory Machine Control Architectures. JSS 81(4), 517–535 (2008)

    Google Scholar 

  13. Groote, J.F., Mathijssen, A.J.H., Reniers, M.A., Usenko, Y.S., van Weerdenburg, M.J.: The Formal Specification Language mCRL2. In: MMOSS. Dagstuhl Seminar Proceedings, vol. 06351. IBFI, Schloss Dagstuhl, Germany (2007)

    Google Scholar 

  14. Horn, A.: On Sentences Which are True of Direct Unions of Algebras. J. Symb. Log. 16(1), 14–21 (1951)

    Article  MathSciNet  MATH  Google Scholar 

  15. IEEE Standard for the Scheme Programming Language. IEEE Std 1178-1990 (1991)

    Google Scholar 

  16. Jackson, E.K., Schulte, W.: Model Generation for Horn Logic with Stratified Negation. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol. 5048, pp. 1–20. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Jackson, E.K., Sztipanovits, J.: Formalizing the structural semantics of domain-specific modeling languages. Software and System Modeling 8(4), 451–478 (2009)

    Article  Google Scholar 

  18. Jansamak, S., Surarerks, A.: Formalization of UML statechart models using Concurrent Regular Expressions. In: ACSC 2004, pp. 83–88. Australian Computer Society, Inc., Darlinghurst (2004)

    Google Scholar 

  19. Kleppe, A.: Software language engineering. Addisson-Wesley (2009)

    Google Scholar 

  20. Kuske, S.: A Formal Semantics of UML State Machines Based on Structured Graph Transformation. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185, pp. 241–256. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  21. Mauw, S., Wiersma, W.T., Willemse, T.J.H.: Language-Driven System Design. IJSEKE 14(6), 625–663 (2004)

    Google Scholar 

  22. Lilius, J., Paltor, I.P.: Formalising UML State Machines for Model Checking. In: France, R.B. (ed.) UML 1999. LNCS, vol. 1723, pp. 430–444. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  23. Plotkin, G.D.: A Structural Approach to Operational Semantics. J. Log. Algebr. Program. 60-61, 17–139 (2004)

    Article  MathSciNet  Google Scholar 

  24. Rumbaugh, J., Jacobson, I., Booch, G.: Unified Modeling Language Reference Manual, 2nd edn. Pearson Higher Education (2004)

    Google Scholar 

  25. Sadilek, D.A., Wachsmuth, G.: Using Grammarware Languages to Define Operational Semantics of Modelled Languages. In: Oriol, M., Meyer, B. (eds.) TOOLS EUROPE 2009. LNBIP, vol. 33, pp. 348–356. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  26. Stappers, F.P.M., Reniers, M.A., Weber, S.: Transforming SOS Specifications to Linear Processes. In: Salaün, G., Schätz, B. (eds.) FMICS 2011. LNCS, vol. 6959, pp. 196–211. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  27. Tonino, H.: A Sound and Complete SOS-Semantics for Non-Distributed Deterministic Abstract State Machines. In: Workshop on Abstract State Machines, pp. 91–110 (1998)

    Google Scholar 

  28. van Beek, D.A., Reniers, M.A., Schiffelers, R.R.H., Rooda, J.E.: Foundations of a Compositional Interchange Format for Hybrid Systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 587–600. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  29. van den Nieuwelaar, N.J.M.: Supervisory Machine Control by Predictive-reactive Scheduling. PhD thesis, Technische University Eindhoven (2004)

    Google Scholar 

  30. Wielemaker, J.: An Overview of the SWI-Prolog Programming Environment. In: WLPE. Report, vol. CW371, pp. 1–16. Katholieke Universiteit Leuven (2003)

    Google Scholar 

  31. Wolterink, T.J.L.: Operational Semantics Applied to Model Driven Engineering. Master’s thesis, University of Twente (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Mathematics and Computer Science, Eindhoven University of Technology, P.O. Box 513, NL-5600 MB, Eindhoven, The Netherlands

    Frank P. M. Stappers, Suzana Andova & Istvan Nagy

  2. Dept. for Architecture and Platform, ASML, P.O. Box 324, NL-5500 AH, Veldhoven, The Netherlands

    Sven Weber & Istvan Nagy

  3. Dept. of Mechanical Engineering, Eindhoven University of Technology, P.O. Box 513, NL-5600 MB, Eindhoven, The Netherlands

    Michel A. Reniers

Authors
  1. Frank P. M. Stappers
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sven Weber
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michel A. Reniers
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Suzana Andova
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Istvan Nagy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing, Macquarie University, 2109, Sydney, NSW, Australia

    Anthony Sloane

  2. Fakultät Informatik, Institut für Software- und Multimediatechnik (SMT), Technische Universität Dresden, Nöthnitzer Straße 46, 01062, Dresden, Germany

    Uwe Aßmann

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Stappers, F.P.M., Weber, S., Reniers, M.A., Andova, S., Nagy, I. (2012). Formalizing a Domain Specific Language Using SOS: An Industrial Case Study. In: Sloane, A., Aßmann, U. (eds) Software Language Engineering. SLE 2011. Lecture Notes in Computer Science, vol 6940. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28830-2_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-28830-2_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-28829-6

  • Online ISBN: 978-3-642-28830-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation