Skip to main content
SpringerLink
Log in

Automated Specification Extraction and Analysis with Specstractor

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10886))

Included in the following conference series:

  • 744 Accesses

Abstract

This paper presents Specstractor, a tool chain for the extraction and analysis of system specifications in the form of collections of invariants. Such invariants convey valuable information about the behavior of a software system and are also useful in identifying missing or defective parts of existing specifications. Using data-mining techniques, Specstractor derives likely invariants from test data that it automatically generates from the system under analysis, using an iterative approach to refine the set of proposed invariants and eliminate false positives. The paper describes the Spectstractor technology and evaluates it on real-world artifacts from automotive-control and medical-device applications.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In fact, it is common practice in these applications not to use C-function inputs and outputs, but instead use other external variables for this purpose.

  2. 2.

    Reactis® and Reactis for C® are registered trademarks of Reactive Systems, Inc.

References

  1. Ackermann, C., Cleaveland, R., Huang, S., Ray, A., Shelton, C., Latronico, E.: Automatic requirement extraction from test cases. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 1–15. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_1

    Chapter  Google Scholar 

  2. Ernst, M.D., et al.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69, 35–45 (2007)

    Article  MathSciNet  Google Scholar 

  3. Cheng, X., Hsiao, M.S.: Simulation-directed invariant mining for software verification. In: Proceedings of DATE 2008, pp. 682–687. ACM, New York (2008)

    Google Scholar 

  4. Beschastnikh, I., et al.: Mining temporal invariants from partially ordered logs. In: SLAML 2011, pp. 3:1–3:10. ACM, New York (2011)

    Google Scholar 

  5. Schulze, C., Cleaveland, R.: Improving invariant mining via static analysis. ACM Trans. Embed. Comput. Syst. 16, 167:1–167:20 (2017)

    Article  Google Scholar 

  6. Han, J., Pei, J., Yin, Y.: Mining frequent patterns without candidate generation. In: ACM SIGMOD Record, vol. 29, pp. 1–12. ACM (2000)

    Google Scholar 

  7. Fournier-Viger, P., Lin, J.C.-W., Gomariz, A., Gueniche, T., Soltani, A., Deng, Z., Lam, H.T.: The SPMF open-source data mining library version 2. In: Berendt, B., Bringmann, B., Fromont, É., Garriga, G., Miettinen, P., Tatti, N., Tresp, V. (eds.) ECML PKDD 2016. LNCS (LNAI), vol. 9853, pp. 36–40. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46131-1_8

    Chapter  Google Scholar 

  8. Cleaveland, R., Smolka, S.A., Sims, S.T.: An instrumentation-based approach to controller model validation. In: Broy, M., Krüger, I.H., Meisinger, M. (eds.) ASWSD 2006. LNCS, vol. 4922, pp. 84–97. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70930-5_6

    Chapter  Google Scholar 

  9. Agrawal, R., Srikant, R., et al.: Fast algorithms for mining association rules. Proc. VLDB 1215, 487–499 (1994)

    Google Scholar 

  10. Srikant, R., Agrawal, R.: Mining quantitative association rules in large relational tables. In: Proceedings of SIGMOD, pp. 1–12. ACM, New York (1996)

    Google Scholar 

  11. Salleb-Aouissi, A., Vrain, C., Nortet, C.: Quantminer: a genetic algorithm for mining quantitative association rules. IJCAI 7, 1035–1040 (2007)

    MATH  Google Scholar 

  12. Han, J., Pei, J., Kamber, M.: Data Mining: Concepts and Techniques. Elsevier, New York (2011)

    MATH  Google Scholar 

  13. Bay, S.D.: Multivariate discretization for set mining. Knowl. Inf. Syst. 3(4), 491–512 (2001)

    Article  Google Scholar 

  14. Kellerer, H., Pferschy, U., Pisinger, D.: Introduction to NP-completeness of knapsack problems. In: Knapsack Problems, pp. 483–493. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24777-7_16

  15. Lindvall, M., et al.: Safety-focused security requirements elicitation for medical device software. In: Requirements Engineering, pp. 134–143. IEEE (2017)

    Google Scholar 

  16. Merten, M., Steffen, B., Howar, F., Margaria, T.: Next generation learnlib. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 220–223. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_18

    Chapter  Google Scholar 

  17. Rozier, K.Y.: Specification: the biggest bottleneck in formal methods and autonomy. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 8–26. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48869-1_2

    Chapter  Google Scholar 

  18. Zeller, A.: Specifications for free. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 2–12. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_2

    Chapter  Google Scholar 

  19. Dallmeier, V., Knopp, N., Mallon, C., Hack, S., Zeller, A.: Generating test cases for specification mining. In: Proceedings of ISSTA, p. 85. ACM Press, July 2010

    Google Scholar 

  20. Le Goues, C., Weimer, W.: Specification mining with few false positives. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 292–306. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_26

    Chapter  Google Scholar 

  21. Lorenzoli, D., Mariani, L., Pezzè, M.: Automatic generation of software behavioral models. In: Proceedings of ICSE, p. 501. ACM Press, May 2008

    Google Scholar 

  22. Vasudevan, S., et al.: GoldMine: automatic assertion generation using data mining and static analysis. In: Proceedings of DATE, pp. 626–629 (2010)

    Google Scholar 

  23. Zeng, F., Cao, Q., Mao, L., Chen, Z.: Test case generation based on invariant extraction. In: Proceedings of WCNMC, pp. 1–4. IEEE, September 2009

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Maryland, College Park, MD, 20742, USA

    Christoph Schulze & Rance Cleaveland

  2. Fraunhofer Center for Experimental Software Engineering, College Park, MD, 20742, USA

    Christoph Schulze & Mikael Lindvall

Authors
  1. Christoph Schulze
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rance Cleaveland
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mikael Lindvall
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Rance Cleaveland .

Editor information

Editors and Affiliations

  1. University of Oslo, Oslo, Norway

    Einar Broch Johnsen

  2. Braunschweig University of Technology, Braunschweig, Germany

    Ina Schaefer

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Schulze, C., Cleaveland, R., Lindvall, M. (2018). Automated Specification Extraction and Analysis with Specstractor. In: Johnsen, E., Schaefer, I. (eds) Software Engineering and Formal Methods. SEFM 2018. Lecture Notes in Computer Science(), vol 10886. Springer, Cham. https://doi.org/10.1007/978-3-319-92970-5_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-92970-5_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-92969-9

  • Online ISBN: 978-3-319-92970-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation