Automatic Generation of DO-178 Test Procedures

  • César Ochoa EscuderoEmail author
  • Rémi Delmas
  • Thomas Bochot
  • Matthieu David
  • Virginie Wiels
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10811)


The work presented in this paper takes place in the context of the testing activities of safety critical Air Management Systems for civilian and military aircraft. The applicative software of such systems is developed following DO-178 guidelines, using a model-based approach built on the SCADE modeling language. In the current V&V process, Test Cases (TCs) specify test conditions and expected outcomes on internal data-flows of the SCADE model. TCs are then implemented in the form of concrete Test Procedures (TPs) that are run against the executable object code and can thus only drive the main inputs of the program. TP implementation is a complex task, today performed manually. This paper proposes an approach to assist the generation of TPs, based on a purpose-built domain specific language for test case specification, from which synchronous observers are generated and composed with the applicative software SCADE model. TPs are then obtained by using a model checker to refute the observer output, yielding, after some post-processing a trace of main input values extended with expected outcome checks.


Software testing Domain-specific language Synchronous observers Model-checking 


  1. 1.
  2. 2.
    Systerel Smart Solver. Accessed 6 Feb 2018
  3. 3.
    Beneviste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Le Guernie, P., de Simone, R.: The synchronous languages 12 years later. Proc. IEEE 91(1), 64–83 (2003)CrossRefGoogle Scholar
  4. 4.
    Colaço, J.L., Pagano, B., Pouzet. M.: A conservative extension of synchronous data-flow with state machines (2005)Google Scholar
  5. 5.
    De Giacomo, G., De Masellis, R., Montali, M.: Reasoning on LTL on finite traces: insensitivity to infiniteness (2014)Google Scholar
  6. 6.
    De Giacomo, G., De Masellis, R., Grasso, M., Maggi, F.M., Montali, M.: LTLF and LDLF monitoring: a Technical report (2014)Google Scholar
  7. 7.
    De Giacomo, G., Vardi, M.Y.: Synthesis for LTL and LDL on finite traces (2015)Google Scholar
  8. 8.
    De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces (2013)Google Scholar
  9. 9.
    Du, X., Liu, Y., Tiu, A.: Trace-length independent runtime monitoring of quantitative policies in LTL (2015)Google Scholar
  10. 10.
    Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification (2013)Google Scholar
  11. 11.
    Fionda, V., Greco, G.: The complexity of LTL on finite traces: hard and easy fragments (2016)Google Scholar
  12. 12.
    Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming lanagage Lustre. Proc. IEEE 79(9), 1305–1320 (1991)CrossRefGoogle Scholar
  13. 13.
    Kurtev, I., Hooman, J., Schuts, M.: Runtime monitoring based on interface specifications. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 335–356. Springer, Cham (2017). CrossRefGoogle Scholar
  14. 14.
    Leucker, M., Schallhart, C.: A brief account of runtime verification (2009)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • César Ochoa Escudero
    • 1
    • 2
    Email author
  • Rémi Delmas
    • 1
  • Thomas Bochot
    • 2
  • Matthieu David
    • 2
  • Virginie Wiels
    • 1
  1. 1.ONERAToulouseFrance
  2. 2.Liebherr-Aerospace Toulouse SASToulouseFrance

Personalised recommendations