Abstract
We are interested in specifications which provide a consistent high-level view of systems. They should abstract irrelevant details and provide a precise and complete description of the behaviour of the system. This view of software specification can naturally be expressed by means of Gurevich’s Abstract State Machines (ASMs). There are many known benefits of such an approach to system specifications for software engineering and testing. In practice however, such specifications are rarely generated and/or maintained during software development. Addressing this problem, we present an exploratory study on (semi) automated extraction of high-level software specifications by means of ASMs. We describe, in the form of examples, an abstraction process which starts by extracting an initial ground-level ASM specification from Java source code (with the same core functionality), and ends in a high-level ASM specification at the desired level of abstraction. We argue that this process can be done in a (semi) automated way, resulting in a valuable tool to improve the current software engineering practices.
The research reported in this paper results from the project Higher-Order Logics and Structures supported by the Austrian Science Fund (FWF: [I2420-N31]). It was further supported by the Austrian Ministry for Transport, Innovation and Technology, the Federal Ministry of Science, Research and Economy, and the Province of Upper Austria in the frame of the COMET center SCCH.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Barnett, M., Börger, E., Gurevich, Y., Schulte, W., Veanes, M.: Using abstract state machines at microsoft: a case study. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 367–379. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44518-8_21
Blass, A., Gurevich, Y.: Abstract state machines capture parallel algorithms. ACM Trans. Comput. Logic 4(4), 578–651 (2003)
Blass, A., Gurevich, Y.: Abstract state machines capture parallel algorithms: correction and extension. ACM Trans. Comput. Logic 9(3), 19:1–19:32 (2008)
Börger, E.: The origins and the development of the ASM method for high level system design and analysis. J. UCS 8(1), 2–74 (2002)
Börger, E.: Abstract state machines: a unifying view of models of computation and of system design frameworks. Ann. Pure Appl. Logic 133(1–3), 149–171 (2005)
Börger, E.: Design pattern abstractions and abstract state machines. In: Proceedings of the 12th International Workshop on Abstract State Machines, ASM 2005, 8–11 March 2005, Paris, France, pp. 91–100 (2005). http://www.univ-paris12.fr/lacl/dima/asm05/DesignPattern.ps
Börger, E., Cisternino, A., Gervasi, V.: Ambient abstract state machines with applications. J. Comput. Syst. Sci. 78(3), 939–959 (2012)
Börger, E., Schewe, K.: Concurrent abstract state machines. Acta Inf. 53(5), 469–492 (2016)
Börger, E., Stärk, R.F.: Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-642-18216-7
Börger, E., Stärk, R.F.: Exploiting abstraction for specification reuse. the Java/C# case study. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 42–76. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30101-1_3
Bowen, J.P., Breuer, P.T., Lano, K.: Formal specifications in software maintenance: from code to z\({}^{\text{++ }}\) and back again. Inf. Softw. Technol. 35(11–12), 679–690 (1993)
Chikofsky, E.J., II, J.H.C.: Reverse engineering and design recovery: a taxonomy. IEEE Softw. 7(1), 13–17 (1990)
Ferrarotti, F., Schewe, K.-D., Tec, L.: A behavioural theory for reflective sequential algorithms. In: Petrenko, A.K., Voronkov, A. (eds.) PSI 2017. LNCS, vol. 10742, pp. 117–131. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-74313-4_10
Ferrarotti, F., Schewe, K., Tec, L., Wang, Q.: A new thesis concerning synchronised parallel computing - simplified parallel ASM thesis. Theor. Comput. Sci. 649, 25–53 (2016)
Fleck, G., et al.: Experience report on building ASTM based tools for multi-language reverse engineering. In: IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering, SANER 2016, Suita, Osaka, Japan, 14–18 March 2016, vol. 1, pp. 683–687 (2016)
Grädel, E., Nowack, A.: Quantum computing and abstract state machines. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 309–323. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36498-6_18
Grieskamp, W., Gurevich, Y., Schulte, W., Veanes, M.: Generating finite state machines from abstract state machines. In: Proceedings of the International Symposium on Software Testing and Analysis, ISSTA 2002, Roma, Italy, 22–24 July 2002, pp. 112–122. ACM (2002)
Gurevich, Y.: Reconsidering turing’s thesis: toward more realistic semantics of programs. Technical Report CRL-TR-36-84, January 1984
Gurevich, Y.: A new thesis. Technical Report 85T–68-203, abstracts, American Mathematical Society (1985)
Gurevich, Y.: Sequential abstract-state machines capture sequential algorithms. ACM Trans. Comput. Logic 1(1), 77–111 (2000)
Habrias, H., Frappier, M.: Software Specification Methods. ISTE (2006)
Izquierdo, J.L.C., Molina, J.G.: Extracting models from source code in software modernization. Softw. Syst. Model. 13(2), 713–734 (2014)
Lano, K., Breuer, P.T., Haughton, H.P.: Reverse-engineering COBOL via formal methods. J. Softw. Maintenance 5(1), 13–35 (1993)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Ferrarotti, F., Pichler, J., Moser, M., Buchgeher, G. (2019). Extracting High-Level System Specifications from Source Code via Abstract State Machines. In: Schewe, KD., Singh, N. (eds) Model and Data Engineering. MEDI 2019. Lecture Notes in Computer Science(), vol 11815. Springer, Cham. https://doi.org/10.1007/978-3-030-32065-2_19
Download citation
DOI: https://doi.org/10.1007/978-3-030-32065-2_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-32064-5
Online ISBN: 978-3-030-32065-2
eBook Packages: Computer ScienceComputer Science (R0)