|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
| | ||
| Search | ||
| ||
2012 IEEE Fifth International Conference on Software Testing, Verification and Validation
Formal Model-Based Test for AUTOSAR Multicore RTOS
Montreal, Quebec Canada
April 17-April 21
ISBN: 978-0-7695-4670-4
| ASCII Text | x | ||
| Ling Fang, Takashi Kitamura, Thi Bich Ngoc Do, Hitoshi Ohsaki, "Formal Model-Based Test for AUTOSAR Multicore RTOS," Software Testing, Verification, and Validation, 2008 International Conference on, pp. 251-259, 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation, 2012. | |||
| BibTex | x | ||
| @article{ 10.1109/ICST.2012.105, author = {Ling Fang and Takashi Kitamura and Thi Bich Ngoc Do and Hitoshi Ohsaki}, title = {Formal Model-Based Test for AUTOSAR Multicore RTOS}, journal ={Software Testing, Verification, and Validation, 2008 International Conference on}, volume = {0}, year = {2012}, isbn = {978-0-7695-4670-4}, pages = {251-259}, doi = {http://doi.ieeecomputersociety.org/10.1109/ICST.2012.105}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Software Testing, Verification, and Validation, 2008 International Conference on TI - Formal Model-Based Test for AUTOSAR Multicore RTOS SN - 978-0-7695-4670-4 SP251 EP259 A1 - Ling Fang, A1 - Takashi Kitamura, A1 - Thi Bich Ngoc Do, A1 - Hitoshi Ohsaki, PY - 2012 KW - AUTOSAR multicore RTOS KW - model checking KW - SPIN KW - model-based test KW - test automation VL - 0 JA - Software Testing, Verification, and Validation, 2008 International Conference on ER - | |||
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICST.2012.105
AUTOSAR multicore RTOS is a safety-critical concurrent system, for which high quality is required. A conformance test is important to ensure the quality of the software, but the conventional test is low in coverage and high in cost. In this paper, we present a formal model-based test for multicore RTOS that supports AUTOSAR specifications. First, we developed a formal model. With the model, we developed a test case generator, from which an entire test suite can be extracted. Moreover, we proposed a test program generator, with which optimal executable test programs can be generated fully automatically. Both of the generators are assisted with model checking on the formal model. Bug analysis also becomes easy. Our method demonstrated its advantage over conventional testing by finding 33 test cases for three system service calls, whereas a conventional test carried out by a development team found only 10 test cases. Our method can improve the coverage of the test, clearly saving in cost and development time. It is expected to significantly improve the testing of the AUTOSAR multicore RTOS.
Index Terms:
AUTOSAR multicore RTOS, model checking, SPIN, model-based test, test automation
Citation:
Ling Fang, Takashi Kitamura, Thi Bich Ngoc Do, Hitoshi Ohsaki, "Formal Model-Based Test for AUTOSAR Multicore RTOS," icst, pp.251-259, 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation, 2012
Usage of this product signifies your acceptance of the Terms of Use.
