Practical Formal Verification of Domain-Specific Language Applications

  • Greg Eakman
  • Howard ReubensteinEmail author
  • Tom Hawkins
  • Mitesh Jain
  • Panagiotis Manolios
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)


An application developer’s primary task is to produce performant systems that meet their specifications. Formal methods techniques allow engineers to create models and implementations that have a high assurance of satisfying a specification. In this experience report, we take a model-based approach to software development that adds the assurance of formal methods to software construction while automating over 90% of the formal modeling. We discuss a software development methodology and two specific examples that illustrate how to integrate formal methods and their benefits into a traditional (testing-based) software development process.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abdelhalim, I., Schneider, S., Treharne, H.: Towards a practical approach to check UML/fUML models consistency using CSP. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 33–48. Springer, Heidelberg (2011) Google Scholar
  2. 2.
  3. 3.
    Amálio, N., Stepney, S., Polack, F.: Formal proof from UML models. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 418–433. Springer, Heidelberg (2004) Google Scholar
  4. 4.
    Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: a challenging model transformation. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MoDELS 2007. LNCS, vol. 4735, pp. 436–450. Springer, Heidelberg (2007) Google Scholar
  5. 5.
    Chamarthi, H.R., Dillinger, P., Manolios, P., Vroon, D.: The ACL2 sedan theorem proving system. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 291–295. Springer, Heidelberg (2011) Google Scholar
  6. 6.
    Chamarthi, H.R., Dillinger, P.C., Manolios, P.: Data definitions in the ACL2 Sedan. In: ACL2 Workshop. EPTCS, vol. 152, pp. 27–48 (2014)Google Scholar
  7. 7.
  8. 8.
    Hardin, D.S., Davis, J.A., Greve, D.A., McClurg, J.R.: Development of a translator from LLVM to ACL2. EPTCS, vol. 152Google Scholar
  9. 9.
    Jackson, D.: Software Abstractions: logic, language, and analysis. MIT press (2012)Google Scholar
  10. 10.
    Jüllig, R., Srinivas, Y., Liu, J.: SPECWARE: an advanced environment for the formal development of complex software systems. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 551–554. Springer, Heidelberg (1996) Google Scholar
  11. 11.

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Greg Eakman
    • 1
  • Howard Reubenstein
    • 1
    Email author
  • Tom Hawkins
    • 1
  • Mitesh Jain
    • 2
  • Panagiotis Manolios
    • 2
  1. 1.BAE SystemsBurlingtonUSA
  2. 2.Northeastern UniversityBostonUSA

Personalised recommendations