Advertisement

Modeling with Scala

  • Klaus HavelundEmail author
  • Rajeev Joshi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11244)

Abstract

The activities and the associated formalisms for modeling and programming have many commonalities. In this paper we emphasize this point of view by modeling two examples in the programming language Scala, which have previously been modeled in the VDM specification language, and the Promela modeling language of the SPIN model checker respectively. The latter Scala model uses an internal DSL for hierarchical state machines, and a simple randomized testing framework exposing the same errors as found with SPIN. We believe, as the examples illustrate, that this use of a modern programming language for modeling is promising, especially if utilizing internal DSLs.

References

  1. 1.
    Barringer, H., Havelund, K.: TraceContract: a Scala DSL for trace analysis. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 57–72. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-21437-0_7CrossRefGoogle Scholar
  2. 2.
    Bjørner, D.: Formalization of data base models. In: Bjørner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 144–215. Springer, Heidelberg (1980).  https://doi.org/10.1007/3-540-10007-5_37CrossRefGoogle Scholar
  3. 3.
    Bjørner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language. LNCS, vol. 61. Springer, Heidelberg (1978).  https://doi.org/10.1007/3-540-08766-4CrossRefzbMATHGoogle Scholar
  4. 4.
    Broy, M., Havelund, K., Kumar, R.: Towards a unified view of modeling and programming. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 238–257. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47169-3_17CrossRefGoogle Scholar
  5. 5.
    Broy, M., Havelund, K., Kumar, R., Steffen, B.: Towards a unified view of modeling and programming (track summary). In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 3–10. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47169-3_17CrossRefGoogle Scholar
  6. 6.
    Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object-Oriented Systems. Springer-Verlag TELOS, Santa Clara (2005)zbMATHGoogle Scholar
  7. 7.
  8. 8.
    Havelund, K.: Closing the gap between specification and programming: VDM\(^{++}\) and Scala. In: Korovina, M., Voronkov, A., (Eds.), HOWARD-60: Higher-Order Workshop on Automated Runtime Verification and Debugging, vol. 1 of EasyChair Proceedings, Manchester, UK, December 2011Google Scholar
  9. 9.
    Havelund, K.: Data automata in Scala. In: Proceedings of the 8th International Symposium on Theoretical Aspects of Software Engineering (TASE 2014) (2014)Google Scholar
  10. 10.
    Havelund, K.: Monitoring with data automata. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 254–273. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-45231-8_18CrossRefGoogle Scholar
  11. 11.
    Havelund, K.: Rule-based runtime verification revisited. Softw. Tools Technol. Transf. (STTT) 17, 143–170 (2015)CrossRefGoogle Scholar
  12. 12.
    Havelund, K., Joshi, R.: Modeling and monitoring of hierarchical state machines in Scala. In: Romanovsky, A., Troubitsyna, E.A. (eds.) SERENE 2017. LNCS, vol. 10479, pp. 21–36. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-65948-0_2CrossRefGoogle Scholar
  13. 13.
    Havelund, K., Lowry, M.R., Penix, J.: Formal analysis of a space-craft controller using SPIN. IEEE Trans. Softw. Eng. 27(8), 749–765 (2001)CrossRefGoogle Scholar
  14. 14.
    Holzmann, G.: The SPIN Model Checker. Addison-Wesley, Boston (2004)Google Scholar
  15. 15.
    Kauffman, S., Havelund, K., Joshi, R.: nfer – a notation and system for inferring event stream abstractions. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 235–250. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-46982-9_15CrossRefGoogle Scholar
  16. 16.
    Pell, B., Gat, E., Keesing, R., Muscettola, N., Smith, B.: Plan execution for autonomous spacecrafts. In: Proceedings of the International Joint Conference on Artificial Intelligence, Nagoya, Japan, August 1997Google Scholar
  17. 17.
  18. 18.
    Samek, M.: Practical UML Statecharts in C/C++, Second Edition: Event-Driven Programming for Embedded Systems, 2nd edn. Newnes, MA (2009)Google Scholar
  19. 19.
  20. 20.

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Jet Propulsion Laboratory, California Institute of TechnologyPasadenaUSA

Personalised recommendations