We present in this paper a way to produce test suites for the POSIX mini-challenge, based on a formal model of a file system manager, written using a B machine. By this case study, we illustrate the limitations of a fully-automated testing process, which justifies the use of scenarios that complements the classical functional testing approach. Scenarios are expressed through schemas, focusing only on operation chaining. They are played on the model using a symbolic animation engine in order to automatically compute pertinent operation parameter values, based on model coverage criteria such as behavioral or data coverage. We concretize our experimentation by testing the POSIX conformance of two different file systems: a recent Linux distribution, and a customized Java implementation of POSIX used to evaluate the relevance of our approach.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{DadeauKT08,
author = {Fr{\'{e}}d{\'{e}}ric Dadeau and
Adrien De Kermadec and
R{\'{e}}gis Tissot},
editor = {Egon B{\"{o}}rger and
Michael J. Butler and
Jonathan P. Bowen and
Paul Boca},
title = {Combining Scenario- and Model-Based Testing to Ensure {POSIX} Compliance},
booktitle = {Abstract State Machines, {B} and Z, First International Conference,
{ABZ} 2008, London, UK, September 16-18, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5238},
pages = {153--166},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-87603-8\_13},
doi = {10.1007/978-3-540-87603-8\_13},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/DadeauKT08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}