Modelling Without a Modelling Language
Valmari, A., & Lappalainen, V. (2018). Modelling Without a Modelling Language. In M. D. M. Gallardo, & P. Merino (Eds.), SPIN 2018 : Model Checking Software (pp. 308-327). Springer. Lecture Notes in Computer Science, 10869. https://doi.org/10.1007/978-3-319-94111-0_18
Published inLecture Notes in Computer Science
© Springer International Publishing AG, part of Springer Nature 2018
Developments in computer hardware and programming languages, in this case C++, have made it feasible to write models of concurrent systems under verification in the programming language, instead of some established modelling language such as Promela. While this does not reduce the usefulness of modelling languages, it offers new possibilities that may be advantageous, for instance, when teaching state space ideas to newcomers or when experimenting with new scientific ideas. In earlier work, we were able to express everything else fairly naturally in C++, except the set of transitions. The present study uses C++ lambda functions to represent naturally transitions that consist of a tail state, guard, body, and head state. We discuss two implementations, a simple one and a faster one. We present measurements demonstrating that the loss of performance compared to the earlier approach is not big. Starting to use our approach is easy, because one only needs to have a C++ compiler and download (not install) one C++ file. ...
Parent publication ISBN978-3-319-94110-3
ConferenceInternational Symposium on Model Checking Software
Is part of publicationSPIN 2018 : Model Checking Software
Publication in research information system
MetadataShow full item record
Showing items with similar title or keywords.
Explicit behavioral detection of visual changes develops without their implicit neurophysiological detectability Lyyra, Pessi; Wikgren, Jan; Ruusuvirta, Timo; Astikainen, Piia (Frontiers Research Foundation, 2012)Change blindness is a failure of reporting major changes across consecutive images if separated, e.g., by a brief blank interval. Successful change detection across interrupts requires focal attention to the changes. ...
Urtamo, Kimmo (2015)Tässä tutkielmassa tutustutaan mobiilikieliin, älypuhelinsovellusten käyttöliittymämalleihin sekä mobiilisuunnittelussa käytettyihin prototyyppeihin. Mobiilikielistä esillä ovat Java, Objective-C ja Qt. Tutkielman aikana ...
The extent of empirical evidence that could inform evidence-based design of programming languages : a systematic mapping study Kaijanaho, Antti-Juhani (University of Jyväskylä, 2014)
Kaijanaho, Antti-Juhani (University of Jyväskylä, 2015)Background: Programming language design is not usually informed by empirical studies. In other ﬁelds similar problems have inspired an evidence-based paradigm of practice. Such a paradigm is practically inevitable in ...
Kaijanaho, Antti-Juhani (ACM, 2017)Programming language research is becoming method conscious. Rigorous mathematical or empirical evaluation is often demanded, which is a good thing. However, I argue in this essay that concept analysis is a legitimate ...