Conformance Checking and Pushdown Reactive Systems
DOI:
https://doi.org/10.19153/cleiej.25.3.2Keywords:
Conformance checking, Test completeness, Reactive systems, Infinite memoryAbstract
Due to their asynchronous interactions, testing reactive systems is a laborious activity present in any software development project.
In this setting, the finite memory formalism of Labeled Transition Systems has been used to generate test suites that can be applied to check ioco conformance of implementations to a given specification.
In this work we turn to a more complex scenario where a stronger formalism is considered, the Visibly Pushdown Labeled Transition System (VPTS), which allows access to a potentially infinite pushdown memory.
We study an extension of the ioco conformance relation to VPTS models and develop polynomial time algorithms to verify conformance for VPTS models in a white-box testing scenario.
References
bibitem{Gargantini05CTES}
A.~Gargantini, ``Conformance testing,'' in emph{Model-Based Testing of
Reactive Systems: Advanced Lectures}, ser. Lecture Notes in Computer Science,
M.~Broy, B.~Jonsson, J.-P. Katoen, M.~Leucker, and A.~Pretschner, Eds., vol.
hskip 1em plus 0.5em minus 0.4emrelax Springer-Verlag, 2005, pp.
--111.
bibitem{sidhu89}
D.~P. Sidhu and T.~Leung, ``Formal methods for protocol testing: A detailed
study,'' emph{IEEE Trans. Softw. Eng.}, vol.~15, no.~4, pp. 413--426, 1989.
bibitem{tret-model-2008}
J.~Tretmans, ``Model based testing with labelled transition systems,'' in
emph{Formal Methods and Testing}, 2008, pp. 1--38.
bibitem{ananbcc-orchestrated-2013}
BIBentryALTinterwordspacing
S.~Anand, E.~K. Burke, T.~Y. Chen, J.~Clark, M.~B. Cohen, W.~Grieskamp,
M.~Harman, M.~J. Harrold, P.~McMinn, and {others}, ``An orchestrated survey
of methodologies for automated software test case generation,'' emph{Journal
of Systems and Software}, vol.~86, no.~8, pp. 1978--2001, 2013. [Online].
Available:
url{http://www.sciencedirect.com/science/article/pii/S0164121213000563}
BIBentrySTDinterwordspacing
bibitem{simap-generating-2014}
BIBentryALTinterwordspacing
A.~Sim~ao and A.~Petrenko, ``Generating complete and finite test suite for
ioco is it possible?'' in emph{Ninth Workshop on Model-Based Testing (MBT
}, 2014, pp. 56--70. [Online]. Available:
url{http://arxiv.org/abs/1403.7261}
BIBentrySTDinterwordspacing
bibitem{bonifacio2020cleiej}
BIBentryALTinterwordspacing
A.~L. Bonifacio and A.~V. Moura, ``Testing asynchronous reactive systems:
Beyond the ioco framework,'' emph{CLEI Electronic Journal}, vol.~24, no.~13,
July 2021. [Online]. Available: url{https://doi.org/10.19153/cleiej.24.2.13}
BIBentrySTDinterwordspacing
bibitem{alurm-visibly-2004}
BIBentryALTinterwordspacing
R.~Alur and P.~Madhusudan, ``Visibly pushdown languages,'' in emph{Proceedings
of the Thirty-sixth Annual ACM Symposium on Theory of Computing}, ser. STOC
'04.hskip 1em plus 0.5em minus 0.4emrelax New York, NY, USA: ACM, 2004, pp.
--211. [Online]. Available:
url{http://doi.acm.org/10.1145/1007352.1007390}
BIBentrySTDinterwordspacing
bibitem{Constant07}
C.~Constant, B.~Jeannet, and T.~J'{e}ron, ``Automatic test generation from
interprocedural specifications,'' in emph{Proceedings of the 19th IFIP
TC6/WG6.1 International Conference, and 7th International Conference on
Testing of Software and Communicating Systems}, ser.
TestCom'07/FATES'07.hskip 1em plus 0.5em minus 0.4emrelax Berlin,
Heidelberg: Springer-Verlag, 2007, p. 41–57.
bibitem{Chedor12}
S.~Ch{'e}dor, T.~J{'e}ron, and C.~Morvan, ``Test generation from recursive
tiles systems,'' in emph{Tests and Proofs}, A.~D. Brucker and J.~Julliand,
Eds.hskip 1em plus 0.5em minus 0.4emrelax Berlin, Heidelberg: Springer
Berlin Heidelberg, 2012, pp. 99--114.
bibitem{Esparza00}
J.~Esparza, D.~Hansel, P.~Rossmanith, and S.~Schwoon, ``Efficient algorithms
for model checking pushdown systems,'' in emph{Proceedings of the 12th
International Conference on Computer Aided Verification}, ser. CAV '00.hskip
em plus 0.5em minus 0.4emrelax Berlin, Heidelberg: Springer-Verlag, 2000,
p. 232–247.
bibitem{FinkelWW97}
A.~Finkel, B.~Willems, and P.~Wolper, ``A direct symbolic approach to model
checking pushdown systems,'' in emph{INFINITY}, 1997, pp. 27--37.
bibitem{sipser}
M.~Sipser, emph{Introduction to the Theory of Computation}.hskip 1em plus
5em minus 0.4emrelax International Thomson Publishing, 1996.
Downloads
Published
Issue
Section
License
Copyright (c) 2022 Adilson Bonifacio, Arnaldo Moura
This work is licensed under a Creative Commons Attribution 4.0 International License.
CLEIej is supported by its home institution, CLEI, and by the contribution of the Latin American and international researchers community, and it does not apply any author charges whatsoever for submitting and publishing. Since its creation in 1998, all contents are made publicly accesibly. The current license being applied is a (CC)-BY license (effective October 2015; between 2011 and 2015 a (CC)-BY-NC license was used).
