Advertisement

Evidential and Continuous Integration of Software Verification Tools

  • Tewodros A. Beyene
  • Harald Ruess
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

The complexity of embedded software and increasing demands on dependability, safety, and security has outpaced the capabilities of current verification and certification methods. In particular traditional verification and certification methods based on manual reviews, process constraints, and testing, which are mandated by current safety standards such as DO-178C [1] and DO-278A [2] for airborne systems and air traffic management systems, ISO 26262 [11] in the automative domain, and IEC 61508 for industrial domains including factory automation and robotics are proving to be overly time- and resource-intensive. For example, costs for developing certification evidence in safety cases according to the DO-178C standard have been shown to range between $50 to $100 per executable line of code, depending on the required safety level [15]. Unless mission-critical embedded software can be developed and verified with less cost and effort, while still satisfying the highest dependability requirements, new mission-critical capabilities such as autonomous control may never reach the market.

References

  1. 1.
    RTCA DO-178C Software Considerations in Airborne Systems and Equipment Certification. RTCA Standard, December 2011Google Scholar
  2. 2.
    RTCA DO-278A Software Integrity Assurance Considerations for Communication, Navigation and Air Traffic Management (CNS/ATM) Systems, December 2011Google Scholar
  3. 3.
    Ábrahám, E., Havelund, K.: Some recent advances in automated analysis. Int. J. Softw. Tools Technol. Transf. 18(2), 121–128 (2016)CrossRefGoogle Scholar
  4. 4.
    Cruanes, S., Hamon, G., Owre, S., Shankar, N.: Tool integration with the evidential tool bus. In: VMCAI (2013)Google Scholar
  5. 5.
    Denney, E., Pai, G.: Evidence arguments for using formal methods in software certification. In: Software Reliability Engineering Workshops (ISSREW), Nov 2013Google Scholar
  6. 6.
    Duvall, P., Matyas, S.M., Glover, A.: Continuous Integration: Improving Software Quality and Reducing Risk. Addison-Wesley Professional, Boston (2007)Google Scholar
  7. 7.
    Groce, A., Havelund, K., Holzmann, G., Joshi, R., Xu, R.-G.: Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning. Ann. Math. Artif. Intell. 70, 315–349 (2014)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Havelund, K., Holzmann, G.J.: Software certification: coding, code, and coders. In: EMSOFT 2011. ACM, New York, NY, USA (2011)Google Scholar
  9. 9.
    Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2011)Google Scholar
  10. 10.
    Holzmann, G.J.: SCRUB: a tool for code reviews, December 2010MathSciNetCrossRefGoogle Scholar
  11. 11.
    ISO: Road vehicles - Functional safety (2011)Google Scholar
  12. 12.
    Kelly, T.P., McDermid, J.A.: Safety case construction and reuse using patterns. In: Software Reliability Engineering Workshops (ISSREW) (1997)CrossRefGoogle Scholar
  13. 13.
    Kroening, D., Tautschnig, M.: CBMC – C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54862-8_26CrossRefGoogle Scholar
  14. 14.
    Moura, L.D., Owre, S., Ruess, H., Rushby, J., Shankar, N.: Integrating verification components. Theories, Tools, Experiments. In: Verified Software (2005)Google Scholar
  15. 15.
    RTI Real-Time Innovations: DDS for Safety-Critical Applications (2014)Google Scholar
  16. 16.
    Rushby. J.: An evidential tool bus. In: Proceedings of ICFEM (2005)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.fortiss — An-Institut Technische Universität MünchenMunichGermany

Personalised recommendations