research-article

Supporting agile development by facilitating natural user interaction with executable formal specifications

Authors:

Timo Nummenmaa,

Aleksi Tiensuu,

Tommi Mikkonen,

Jussi Kuittinen,

Annakaisa KultimaAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 36, Issue 4

Pages 1 - 10

https://doi.org/10.1145/1988997.2003643

Published: 04 August 2011 Publication History

Abstract

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.

References

[1]

Gregory D. Abowd and Alan J. Dix. Integrating status and event phenomena in formal specifications of interactive systems. In Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, SIGSOFT '94, pages 44--52, New York, NY, USA, 1994. ACM.

Digital Library

[2]

Timo Aaltonen, Mika Katara, and Risto Pitkänen. 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.

[3]

T. Aaltonen, M. Katara, and R. Pitkänen. DisCo toolset - the new generation. Journal of Universal Computer Science, 7(1):3--18, 2001.

[4]

S. Black, P.P. Boca, J.P. Bowen, J. Gorman, and M. Hinchey. Formal versus agile: Survival of the fittest. Computer, 42(9):37--45, sept. 2009.

Digital Library

[5]

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.

[6]

J.P. Bowen and M.G. Hinchey. Seven more myths of formal methods. Software, IEEE, 12(4):34--41, jul 1995.

Digital Library

[7]

Eleni Berki, Kerstin V. Siakas, and Elli Georgiadou. Agile quality or depth of reasoning: applicability versus suitability respecting stakeholders' needs. In Ioannis G. Stamelos and Panagiotis Sfetsos, editors, Agile software development quality assurance, pages 23--55. Information Science Reference, London, 2007.

[8]

Eleni Berki and Juri Valtanen. Critical and creative mathematical thinking with practical problem solving skills- a new old challenge. 2008.

[9]

Antoni Diller. Z - An introduction to formal methods. John Wiley & Sons, 1990.

Digital Library

[10]

Dimitris Dranidis and Kalliopi Tigka, editors. Proceedings of the 1st South-East European Workshop on Formal Methods, SEEFM'03, 2003.

[11]

A. Hussey. Formal object-oriented user-interface design. In Software Engineering Conference, 2000. Proceedings. 2000 Australian, 2000.

Digital Library

[12]

Robert J. K. Jacob. Using formal specifications in the design of a human-computer interface. Commun. ACM, 26(4):259--264, 1983.

Digital Library

[13]

H.-M. Järvinen and R. Kurki-Suonio. The DisCo language and temporal logic of actions. Technical report, Tampere University of Technology, Software Systems Laboratory, 1990.

[14]

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.

[15]

John C. Knight, Colleen L. DeJong, Matthew S. Gibble, and Luís G. Nakano. Why are formal methods not used more widely? In Fourth NASA Formal Methods Workshop, pages 1--12, 1997.

[16]

Reino Kurki-Suonio. A Practical Theory of Reactive Systems: Incremental Modeling of Dynamic Behaviors. Springer, 2005.

Digital Library

[17]

L. Lamport. The temporal logic of actions. ACM Trans. Program. Lang. Syst., 16(3):872--923, 1994.

Digital Library

[18]

T. Mikkonen. A layer-based formalization of an onboard instrument. Technical Report 18, Tampere University of Technology, Software Systems Laboratory, 1998.

[19]

Tommi Mikkonen and Risto Pitkänen. On agility of formal specification. In Proceeding of the 2007 conference on Information Modelling and Knowledge Bases XVIII, pages 1--16, Amsterdam, The Netherlands, The Netherlands, 2007. IOS Press.

Digital Library

[20]

T. Nummenmaa, E. Berki, and T. Mikkonen. Exploring games as formal models. In Formal Methods (SEEFM), 2009 Fourth South-East European Workshop on, pages 60--65, 4-5 2009.

Digital Library

[21]

Timo Nummenmaa, Jussi Kuittinen, and Jussi Holopainen. Simulation as a game design tool. In ACE '09: Proceedings of the International Conference on Advances in Computer Enterntainment Technology, pages 232--239, New York, NY, USA, 2009. ACM.

Digital Library

[22]

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.

[23]

Timo Nummenmaa. A method for modeling probabilistic object behaviour for simulations of formal specifications. In Juhan Ernits Tarmo Uustalu, Jüri Vain, editor, Proc. 20th Nordic Workshop on Programming Theory (Extended Abstracts) (NWPT 2008), pages 66--68, Tallinn, Estonia, November 2008.

[24]

M.W. Rohrer. Seeing is believing: the importance of visualization in manufacturing simulation. In Simulation Conference Proceedings, 2000. Winter, volume 2, pages 1211--1216 vol.2, 2000.

Digital Library

[25]

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.

[26]

Ioannis G. Stamelos and Panagiotis Sfetsos. Agile Software Development Quality Assurance. IGI Global, feb 2007.

Digital Library

[27]

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.

[28]

F. TED TSCHANG. Videogames as interactive experiential products and their manner of development. International Journal of Innovation Management, 9(1):103--131, 2005.

Cited By

Basile Dter Beek MFerrari ALegay A(2022)Exploring the ERTMS/ETCS full moving block specification: an experience with formal methodsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-022-00653-324:3(351-370)Online publication date: 1-Jun-2022
https://dl.acm.org/doi/10.1007/s10009-022-00653-3
Sadri‐Moshkenani ZBradley JRothermel G(2021)Survey on test case generation, selection and prioritization for cyber‐physical systemsSoftware Testing, Verification and Reliability10.1002/stvr.179432:1Online publication date: 15-Sep-2021
https://doi.org/10.1002/stvr.1794
Georgiadou ESiakas KBerki EEstdale JRahanu HRoss M(2020)The sociocultural dimension of the Software Process Improvement ManifestoJournal of Software: Evolution and Process10.1002/smr.230432:11Online publication date: 10-Nov-2020
https://dl.acm.org/doi/10.1002/smr.2304
Show More Cited By

Index Terms

Supporting agile development by facilitating natural user interaction with executable formal specifications
1. Social and professional topics
  1. Professional topics
    1. Management of computing and information systems
      1. Project and people management
2. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Requirements analysis
    2. Software development process management
  2. Software notations and tools
    1. Software configuration management and version control systems

Recommendations

Adopting to Agile Software Development

Abstract Agile software development can be made successful, but there is no well-defined way how to achieve this. The problem is that the successful adoption of agile methods and practices is a complex process and this process should be customizable for ...
Research of Agile Software Development Based on Formal Methods
MINES '10: Proceedings of the 2010 International Conference on Multimedia Information Networking and Security

Agile software development is a kind of lightweight development method, which can satisfy to the changes of requirements. This paper applies formal methods into agile software development, and investigates the method to adopt the rCOS in agile software ...
Lean-Agile Software Development: Achieving Enterprise Agility

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 36, Issue 4

July 2011

142 pages

ISSN:0163-5948

DOI:10.1145/1988997

Issue’s Table of Contents

Copyright © 2011 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 August 2011

Published in SIGSOFT Volume 36, Issue 4

Check for updates

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
365
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)2

Reflects downloads up to 30 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Basile Dter Beek MFerrari ALegay A(2022)Exploring the ERTMS/ETCS full moving block specification: an experience with formal methodsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-022-00653-324:3(351-370)Online publication date: 1-Jun-2022
https://dl.acm.org/doi/10.1007/s10009-022-00653-3
Sadri‐Moshkenani ZBradley JRothermel G(2021)Survey on test case generation, selection and prioritization for cyber‐physical systemsSoftware Testing, Verification and Reliability10.1002/stvr.179432:1Online publication date: 15-Sep-2021
https://doi.org/10.1002/stvr.1794
Georgiadou ESiakas KBerki EEstdale JRahanu HRoss M(2020)The sociocultural dimension of the Software Process Improvement ManifestoJournal of Software: Evolution and Process10.1002/smr.230432:11Online publication date: 10-Nov-2020
https://dl.acm.org/doi/10.1002/smr.2304
Georgiadou ESiakas KBerki EEstdale JRahanu HRoss M(2019)A STEEPLED Analysis of the SPI ManifestoSystems, Software and Services Process Improvement10.1007/978-3-030-28005-5_16(209-221)Online publication date: 22-Aug-2019
https://doi.org/10.1007/978-3-030-28005-5_16
Diepenbeck MKühne USoeken MGrosse DDrechsler R(2018)Behaviour Driven Development for Hardware DesignIPSJ Transactions on System LSI Design Methodology10.2197/ipsjtsldm.11.2911(29-45)Online publication date: 2018
https://doi.org/10.2197/ipsjtsldm.11.29
Rodrigues PEcar MMenezes Sda Silva JGuedes GRodrigues E(2018)Empirical Evaluation of Formal Method for Requirements Specification in Agile ApproachesProceedings of the XIV Brazilian Symposium on Information Systems10.1145/3229345.3229401(1-8)Online publication date: 4-Jun-2018
https://dl.acm.org/doi/10.1145/3229345.3229401

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents