Abstract
Many software companies still seem to be reluctant to use formal specifications in their development processes. Nevertheless, the trend towards implementing critical business applications in distributed environments makes such applications an attractive target for formal methods. Additionally, the rising complexity also increases the willingness of the development teams to apply formal techniques.
In this paper, we report on our experiences in formally specifying several core components of one of our commercially available products. While writing the formal specification, we experienced several issues that had a noticeable consequences on our work. While most of these issues can be attributed to the specific method and tools we have used, we do consider some of the problems as more general, impeding the practical application of formal methods, especially by non-experts, in large scale industrial development.
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
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: Modeling in Event-B: System and Software Design. Cambridge University Press, New York (2009)
Altenhofen, M., Börger, E.: Concurrent abstract state machines and +CAL programs. In: Recent Trends in Algebraic Development Techniques, pp. 1–17. Springer, Heidelberg (2009) doi 10.1007/978-3-642-03429-9_1
Altenhofen, M., Farahbod, R.: Bârun: A scripting language for coreasm. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ASM 2010. LNCS, vol. 5977, pp. 47–60. Springer, Heidelberg (2010) doi 10.1007/978-3-642-11811-1_5
Altenhofen, M., Friesen, A., Lemcke, J.: ASMs in service oriented architectures. Journal of Universal Computer Science 14(12), 2034–2058 (2008)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec\(\sharp\) programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.L., Muntean, T. (eds.) Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS), pp. 49–69 doi 10.1007/b105030
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. In: Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)
Börger, E., Stärk, R.F.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
Brucker, A.D., Doser, J., Wolff, B.: An mda framework supporting ocl. Electronic Communications of the EASSTÂ 5 (2006)
Brucker, A.D., Wolff, B.: Hol Ocl – A Formal Proof Environment for UML/OCL. In: Fiadeiro, J., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 97–100. Springer, Heidelberg (2008) doi 10.1007/978-3-540-78743-3_8
Brucker, A.D., Wolff, B.: Hol testgen: an interactive test-case generation framework. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 417–420. Springer, Heidelberg (2009) doi 10.1007/978-3-642-00593-0_28
Burrows, M.: The chubby lock service for loosely-coupled distributed systems. In: OSDI ’06: Proceedings of the 7th Symposium on Operating Systems Design and Implementation, pp. 335–350. USENIX Association, Berkeley (2006)
DeCandia, G., Hastorun, D., Jampani, M., Kakulapati, G., Lakshman, A., Pilchin, A., Sivasubramanian, S., Vosshall, P., Vogels, W.: Dynamo: Amazon’s highly available key-value store. ACM SIGOPS Operating Systems Review 41(6), 205–220 (2007) doi 10.1145/1323293.1294281
Farahbod, R., Gervasi, V., Glässer, U.: CoreASM: An extensible ASM execution engine. Fundamenta Informaticae 77(1-2), 71–103 (2007)
Forgy, C.L.: Rete: A fast algorithm for the many patterns/many objects match problem. Artificial Intelligence 19(1), 17–37 (1982) doi:10.1016/0004-3702(82)90020-0
Knuth, D.E.: Literate programming. The Computer Journal 27(2), 97–111 (1984) doi 10.1093/comjnl/27.2.97
Lange, C., McLaughlin, S., Rabe, F.: Flyspeck in a semantic Wiki. In: Lange, C., Schaffert, S., Skaf-Molli, H., Völkel, M. (eds.) SemWiki. CEUR Workshop Proceedings, vol. 360. CEUR-WS.org (2008)
McCarthy, D., Dayal, U.: The architecture of an active database management system. In: SIGMOD ’89: Proceedings of the 1989 ACM SIGMOD International Conference on Management of Data, pp. 215–224. ACM Press, New York (1989) doi 10.1145/67544.66946
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. In: Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.) Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002) doi 10.1007/3-540-45949-9
Venet, A.: A practical approach to formal software verification by static analysis. Ada Lett. XXVIII(1), 92–95 (2008) doi 10.1145/1387830.1387836
Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science. Prentice Hall, Englewood Cliffs (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Altenhofen, M., Brucker, A.D. (2010). Practical Issues with Formal Specifications. In: Kowalewski, S., Roveri, M. (eds) Formal Methods for Industrial Critical Systems. FMICS 2010. Lecture Notes in Computer Science, vol 6371. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15898-8_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-15898-8_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15897-1
Online ISBN: 978-3-642-15898-8
eBook Packages: Computer ScienceComputer Science (R0)