{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T20:06:50Z","timestamp":1779048410403,"version":"3.51.4"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2011,8,4]],"date-time":"2011-08-04T00:00:00Z","timestamp":1312416000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2011,8,4]]},"abstract":"<jats:p>Agile development benefits from fast feedback from various stakeholders. If implemented in a suitable way, formal methods can enhance the agile development process. With an executable formal specification, it is possible to analyse and simulate the behaviour of the target system before it is being built. However, for the users' and developers' natural participation in the development process, it is necessary to use a real end-user interface and bind it to the execution environment being used in the simulations and animations. This requires, though, that the execution model used to simulate the specification is appropriately changed to facilitate the use of these user interfaces. The authors present a formal and flexible method to facilitate natural user interaction with executable specifications through end-user interfaces. This can be considered as an agile and formal way which provides continuous testable software components through frequently communicated stakeholders' views. The method is based on a modification of the execution of the DisCo system, a software for creating and animating formal specifications. Usage of the method is demonstrated through an exploratory study of a game application.<\/jats:p>","DOI":"10.1145\/1988997.2003643","type":"journal-article","created":{"date-parts":[[2011,8,10]],"date-time":"2011-08-10T12:16:22Z","timestamp":1312978582000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Supporting agile development by facilitating natural user interaction with executable formal specifications"],"prefix":"10.1145","volume":"36","author":[{"given":"Timo","family":"Nummenmaa","sequence":"first","affiliation":[{"name":"School of Information Sciences, University of Tampere, Kanslerinrinne, Tampere, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aleksi","family":"Tiensuu","sequence":"additional","affiliation":[{"name":"School of Information Sciences, University of Tampere, Kanslerinrinne, Tampere, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eleni","family":"Berki","sequence":"additional","affiliation":[{"name":"School of Information Sciences, University of Tampere, Kanslerinrinne, Tampere, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tommi","family":"Mikkonen","sequence":"additional","affiliation":[{"name":"Department of Software Systems, Tampere University of Technology, Korkeakoulunkatu, Tampere, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jussi","family":"Kuittinen","sequence":"additional","affiliation":[{"name":"Agora Center, University of Jyv\u00e4skyl\u00e4, Mattilanniemi 2, FI-40014, Jyv\u00e4skyl\u00e4, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Annakaisa","family":"Kultima","sequence":"additional","affiliation":[{"name":"School of Information Sciences, University of Tampere, Kanslerinrinne, Tampere, Finland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,8,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/193173.195293"},{"key":"e_1_2_1_2_1","first-page":"516","volume-title":"Proc. Conference on Software: Theory and Practice, 16th IFIP World Computer Congress 2000","author":"Aaltonen Timo","year":"2000","unstructured":"Timo Aaltonen, Mika Katara, and Risto Pitk\u00e4nen. Verifying real-time joint action specifications using timed automata. In Proc. Conference on Software: Theory and Practice, 16th IFIP World Computer Congress 2000, pages 516--525. Publishing House of Electronics Industry, 2000."},{"issue":"1","key":"e_1_2_1_3_1","first-page":"3","article-title":"DisCo toolset - the new generation","volume":"7","author":"Aaltonen T.","year":"2001","unstructured":"T. Aaltonen, M. Katara, and R. Pitk\u00e4nen. DisCo toolset - the new generation. Journal of Universal Computer Science, 7(1):3--18, 2001.","journal-title":"Journal of Universal Computer Science"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2009.284"},{"key":"e_1_2_1_5_1","first-page":"170","volume-title":"Proceedings of the 1st South-East European Workshop on Formal Methods, SEEFM'03","author":"Berki Eleni","year":"2003","unstructured":"Eleni Berki. Formal metamodelling and agile method engineering in metacase and came tool environments. In Proceedings of the 1st South-East European Workshop on Formal Methods, SEEFM'03, pages 170--188, 2003."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.391826"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.4018\/978-1-59904-216-9.ch002"},{"key":"e_1_2_1_8_1","volume-title":"Critical and creative mathematical thinking with practical problem solving skills- a new old challenge","author":"Berki Eleni","year":"2008","unstructured":"Eleni Berki and Juri Valtanen. Critical and creative mathematical thinking with practical problem solving skills- a new old challenge. 2008."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/533425"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 1st South-East European Workshop on Formal Methods, SEEFM'03","author":"Dranidis Dimitris","year":"2003","unstructured":"Dimitris Dranidis and Kalliopi Tigka, editors. Proceedings of the 1st South-East European Workshop on Formal Methods, SEEFM'03, 2003."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/786776.787254"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2163.358093"},{"key":"e_1_2_1_13_1","volume-title":"The DisCo language and temporal logic of actions. Technical report","author":"J\u00e4rvinen H.-M.","year":"1990","unstructured":"H.-M. J\u00e4rvinen and R. Kurki-Suonio. The DisCo language and temporal logic of actions. Technical report, Tampere University of Technology, Software Systems Laboratory, 1990."},{"key":"e_1_2_1_14_1","unstructured":"M. Katara. Composing DisCo specifications using generic Real-Time events - a mobile robot case study. In J. Penjamin editor Software Technology Proceedings of the Fenno-Ugric Symposium FUSST'99 Technical Report CS 104\/99 pages 75--86 Sagadi Estonia 1999. Tallinn Technical University."},{"key":"e_1_2_1_15_1","first-page":"1","volume-title":"Fourth NASA Formal Methods Workshop","author":"Knight John C.","year":"1997","unstructured":"John C. Knight, Colleen L. DeJong, Matthew S. Gibble, and Lu\u00eds G. Nakano. Why are formal methods not used more widely? In Fourth NASA Formal Methods Workshop, pages 1--12, 1997."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1062420"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_18_1","unstructured":"T. Mikkonen. A layer-based formalization of an onboard instrument. Technical Report 18 Tampere University of Technology Software Systems Laboratory 1998."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1565391.1565393"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEEFM.2009.15"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1690388.1690427"},{"key":"e_1_2_1_22_1","volume-title":"Adding probabilistic modeling to executable formal disco specifications with applications in strategy modeling in multiplayer game design. Master's thesis","author":"Nummenmaa Timo","year":"2008","unstructured":"Timo Nummenmaa. Adding probabilistic modeling to executable formal disco specifications with applications in strategy modeling in multiplayer game design. Master's thesis, University of Tampere, June 2008."},{"key":"e_1_2_1_23_1","first-page":"66","volume-title":"Proc. 20th Nordic Workshop on Programming Theory (Extended Abstracts) (NWPT 2008","author":"Nummenmaa Timo","year":"2008","unstructured":"Timo Nummenmaa. A method for modeling probabilistic object behaviour for simulations of formal specifications. In Juhan Ernits Tarmo Uustalu, J\u00fcri Vain, editor, Proc. 20th Nordic Workshop on Programming Theory (Extended Abstracts) (NWPT 2008), pages 66--68, Tallinn, Estonia, November 2008."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/510378.510552"},{"key":"e_1_2_1_25_1","first-page":"48","volume-title":"Proceedings of the 1st South-East European Workshop on Formal Methods, SEEFM'03","author":"Sfetsos Panagiotis","year":"2003","unstructured":"Panagiotis Sfetsos and Ioannis Stamelos. Formal experimentation for agile formal methods. In Proceedings of the 1st South-East European Workshop on Formal Methods, SEEFM'03, pages 48--56, 2003."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1205181"},{"key":"e_1_2_1_27_1","volume-title":"Games as Services - Final Report, TRIM Research Reports","author":"Sotamaa Olli","year":"2010","unstructured":"Olli Sotamaa and Jaakko Stenros. Understanding the range of player services. In Olli Sotamaa and Tero Karppi, editors, Games as Services - Final Report, TRIM Research Reports. University of Tampere, 2010."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1142\/S1363919605001198"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1988997.2003643","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1988997.2003643","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T19:36:59Z","timestamp":1779046619000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1988997.2003643"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,8,4]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,8,4]]}},"alternative-id":["10.1145\/1988997.2003643"],"URL":"https:\/\/doi.org\/10.1145\/1988997.2003643","relation":{},"ISSN":["0163-5948"],"issn-type":[{"value":"0163-5948","type":"print"}],"subject":[],"published":{"date-parts":[[2011,8,4]]},"assertion":[{"value":"2011-08-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}