Practical Issues with Formal Specifications: Lessons Learned from an Industrial Case Study

By Michael Altenhofen and Achim D. Brucker.

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.

Keywords:
ASM, industrial case study, formal specification

Supplementary material:
[ Slides  ]

Please cite this work as follows:
M. Altenhofen and A. D. Brucker, “Practical issues with formal specifications: Lessons learned from an industrial case study,” in International workshop on formal methods for industrial critical systems (FMICS), S. Kowalewski and M. Roveri, Eds. Heidelberg: Springer-Verlag, 2010, pp. 17–32. doi: 10.1007/978-3-642-15898-8_2. Author copy: https://logicalhacking.com/publications/altenhofen.ea-issues-2010/

BibTeX
@InCollection{ altenhofen.ea:issues:2010,
  author    = {Michael Altenhofen and Achim D. Brucker},
  booktitle = {International Workshop on Formal Methods for Industrial
               Critical Systems (FMICS)},
  language  = {USenglish},
  title     = {Practical Issues with Formal Specifications: Lessons Learned
               from an Industrial Case Study},
  year      = {2010},
  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.},
  keywords  = {ASM, industrial case study, formal specification},
  editor    = {Stefan Kowalewski and Marco Roveri},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  doi       = {10.1007/978-3-642-15898-8_2},
  series    = {Lecture Notes in Computer Science },
  number    = {6371},
  pages     = {17--32},
  areas     = {formal methods},
  note      = {Author copy: \url{https://logicalhacking.com/publications/altenhofen.ea-issues-2010/}},
  pdf       = {https://logicalhacking.com/publications/altenhofen.ea-issues-2010/altenhofen.ea-issues-2010.pdf},
}