Functional Requirements-Based Automated Testing for Avionics. Sun, Y., Brain, M., Kroening, D., Hawthorn, A., Wilson, T., Schanda, F., Jiménez, F. J. G., Daniel, S., Bryan, C., & Broster, I. In 2017 22nd International Conference on Engineering of Complex Computer Systems (ICECCS), pages 170–173, November, 2017. doi abstract bibtex We propose and demonstrate a method for the reduction of testing effort in safety-critical software development using DO-178 guidance. We achieve this through the application of Bounded Model Checking (BMC) to formal low-level requirements, in order to generate tests automatically that are good enough to replace existing labor-intensive test writing procedures while maintaining independence from implementation artefacts. Given that manual processes are often empirical and subjective, we begin by formally defining a metric, which extends recognized best practice from code coverage analysis strategies to generate tests that adequately cover the requirements. We then implement it in an automated requirements testing procedure and apply it in a case study with industrial partners. In review, the toolchain developed here is demonstrated to significantly reduce the human effort for the qualification of software products under DO-178 guidance.
@inproceedings{sun_functional_2017,
title = {Functional {Requirements}-{Based} {Automated} {Testing} for {Avionics}},
doi = {10/ghv5hv},
abstract = {We propose and demonstrate a method for the reduction of testing effort in safety-critical software development using DO-178 guidance. We achieve this through the application of Bounded Model Checking (BMC) to formal low-level requirements, in order to generate tests automatically that are good enough to replace existing labor-intensive test writing procedures while maintaining independence from implementation artefacts. Given that manual processes are often empirical and subjective, we begin by formally defining a metric, which extends recognized best practice from code coverage analysis strategies to generate tests that adequately cover the requirements. We then implement it in an automated requirements testing procedure and apply it in a case study with industrial partners. In review, the toolchain developed here is demonstrated to significantly reduce the human effort for the qualification of software products under DO-178 guidance.},
booktitle = {2017 22nd {International} {Conference} on {Engineering} of {Complex} {Computer} {Systems} ({ICECCS})},
author = {Sun, Y. and Brain, M. and Kroening, D. and Hawthorn, A. and Wilson, T. and Schanda, F. and Jiménez, F. J. G. and Daniel, S. and Bryan, C. and Broster, I.},
month = nov,
year = {2017},
keywords = {BMC, Bounded Model Checking, Compounds, DO-178 guidance, Manuals, Model checking, Software, Syntactics, Tools, automated requirements, automated testing, avionics, code coverage analysis strategies, functional requirements, labor-intensive test writing procedures, low-level requirements, program testing, program verification, safety-critical software, safety-critical software development, software products, testing effort},
pages = {170--173},
}
Downloads: 0
{"_id":"FmA48rr3Xv5dThRrq","bibbaseid":"sun-brain-kroening-hawthorn-wilson-schanda-jimnez-daniel-etal-functionalrequirementsbasedautomatedtestingforavionics-2017","author_short":["Sun, Y.","Brain, M.","Kroening, D.","Hawthorn, A.","Wilson, T.","Schanda, F.","Jiménez, F. J. G.","Daniel, S.","Bryan, C.","Broster, I."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Functional Requirements-Based Automated Testing for Avionics","doi":"10/ghv5hv","abstract":"We propose and demonstrate a method for the reduction of testing effort in safety-critical software development using DO-178 guidance. We achieve this through the application of Bounded Model Checking (BMC) to formal low-level requirements, in order to generate tests automatically that are good enough to replace existing labor-intensive test writing procedures while maintaining independence from implementation artefacts. Given that manual processes are often empirical and subjective, we begin by formally defining a metric, which extends recognized best practice from code coverage analysis strategies to generate tests that adequately cover the requirements. We then implement it in an automated requirements testing procedure and apply it in a case study with industrial partners. In review, the toolchain developed here is demonstrated to significantly reduce the human effort for the qualification of software products under DO-178 guidance.","booktitle":"2017 22nd International Conference on Engineering of Complex Computer Systems (ICECCS)","author":[{"propositions":[],"lastnames":["Sun"],"firstnames":["Y."],"suffixes":[]},{"propositions":[],"lastnames":["Brain"],"firstnames":["M."],"suffixes":[]},{"propositions":[],"lastnames":["Kroening"],"firstnames":["D."],"suffixes":[]},{"propositions":[],"lastnames":["Hawthorn"],"firstnames":["A."],"suffixes":[]},{"propositions":[],"lastnames":["Wilson"],"firstnames":["T."],"suffixes":[]},{"propositions":[],"lastnames":["Schanda"],"firstnames":["F."],"suffixes":[]},{"propositions":[],"lastnames":["Jiménez"],"firstnames":["F.","J.","G."],"suffixes":[]},{"propositions":[],"lastnames":["Daniel"],"firstnames":["S."],"suffixes":[]},{"propositions":[],"lastnames":["Bryan"],"firstnames":["C."],"suffixes":[]},{"propositions":[],"lastnames":["Broster"],"firstnames":["I."],"suffixes":[]}],"month":"November","year":"2017","keywords":"BMC, Bounded Model Checking, Compounds, DO-178 guidance, Manuals, Model checking, Software, Syntactics, Tools, automated requirements, automated testing, avionics, code coverage analysis strategies, functional requirements, labor-intensive test writing procedures, low-level requirements, program testing, program verification, safety-critical software, safety-critical software development, software products, testing effort","pages":"170–173","bibtex":"@inproceedings{sun_functional_2017,\n\ttitle = {Functional {Requirements}-{Based} {Automated} {Testing} for {Avionics}},\n\tdoi = {10/ghv5hv},\n\tabstract = {We propose and demonstrate a method for the reduction of testing effort in safety-critical software development using DO-178 guidance. We achieve this through the application of Bounded Model Checking (BMC) to formal low-level requirements, in order to generate tests automatically that are good enough to replace existing labor-intensive test writing procedures while maintaining independence from implementation artefacts. Given that manual processes are often empirical and subjective, we begin by formally defining a metric, which extends recognized best practice from code coverage analysis strategies to generate tests that adequately cover the requirements. We then implement it in an automated requirements testing procedure and apply it in a case study with industrial partners. In review, the toolchain developed here is demonstrated to significantly reduce the human effort for the qualification of software products under DO-178 guidance.},\n\tbooktitle = {2017 22nd {International} {Conference} on {Engineering} of {Complex} {Computer} {Systems} ({ICECCS})},\n\tauthor = {Sun, Y. and Brain, M. and Kroening, D. and Hawthorn, A. and Wilson, T. and Schanda, F. and Jiménez, F. J. G. and Daniel, S. and Bryan, C. and Broster, I.},\n\tmonth = nov,\n\tyear = {2017},\n\tkeywords = {BMC, Bounded Model Checking, Compounds, DO-178 guidance, Manuals, Model checking, Software, Syntactics, Tools, automated requirements, automated testing, avionics, code coverage analysis strategies, functional requirements, labor-intensive test writing procedures, low-level requirements, program testing, program verification, safety-critical software, safety-critical software development, software products, testing effort},\n\tpages = {170--173},\n}\n\n","author_short":["Sun, Y.","Brain, M.","Kroening, D.","Hawthorn, A.","Wilson, T.","Schanda, F.","Jiménez, F. J. G.","Daniel, S.","Bryan, C.","Broster, I."],"key":"sun_functional_2017","id":"sun_functional_2017","bibbaseid":"sun-brain-kroening-hawthorn-wilson-schanda-jimnez-daniel-etal-functionalrequirementsbasedautomatedtestingforavionics-2017","role":"author","urls":{},"keyword":["BMC","Bounded Model Checking","Compounds","DO-178 guidance","Manuals","Model checking","Software","Syntactics","Tools","automated requirements","automated testing","avionics","code coverage analysis strategies","functional requirements","labor-intensive test writing procedures","low-level requirements","program testing","program verification","safety-critical software","safety-critical software development","software products","testing effort"],"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/SilverSylvester","dataSources":["YCBcQPneB9oxahSnp"],"keywords":["bmc","bounded model checking","compounds","do-178 guidance","manuals","model checking","software","syntactics","tools","automated requirements","automated testing","avionics","code coverage analysis strategies","functional requirements","labor-intensive test writing procedures","low-level requirements","program testing","program verification","safety-critical software","safety-critical software development","software products","testing effort"],"search_terms":["functional","requirements","based","automated","testing","avionics","sun","brain","kroening","hawthorn","wilson","schanda","jiménez","daniel","bryan","broster"],"title":"Functional Requirements-Based Automated Testing for Avionics","year":2017}