MODEL CHECKING IS REFINEMENT - From Computation Tree Logic to Failure Trace Testing

Stefan D. Bruda, Zhiyu Zhang

2010

Abstract

Two major systems of formal conformance testing are model checking and algebraic model-based testing. Model checking is based on some form of temporal logic. One powerful and realistic logic being used is computation tree logic (CTL), which is capable of expressing most interesting properties of processes such as liveness and safety. Model-based testing is based on some operational semantics of processes (such as traces, failures, or both) and associated preorders. The most fine-grained preorder beside bisimulation (mostly of theoretical importance) is based on failure traces. We show that these two powerful variants are equivalent, in the sense that for any CTL formula there exists a set of failure trace tests that are equivalent to it. Combined with previous results, this shows that CTL and failure trace tests are equivalent.

Download


Paper Citation


in Harvard Style

D. Bruda S. and Zhang Z. (2010). MODEL CHECKING IS REFINEMENT - From Computation Tree Logic to Failure Trace Testing . In Proceedings of the 5th International Conference on Software and Data Technologies - Volume 2: ICSOFT, ISBN 978-989-8425-23-2, pages 173-178. DOI: 10.5220/0003006801730178

in Bibtex Style

@conference{icsoft10,
author={Stefan D. Bruda and Zhiyu Zhang},
title={MODEL CHECKING IS REFINEMENT - From Computation Tree Logic to Failure Trace Testing},
booktitle={Proceedings of the 5th International Conference on Software and Data Technologies - Volume 2: ICSOFT,},
year={2010},
pages={173-178},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0003006801730178},
isbn={978-989-8425-23-2},
}


in EndNote Style

TY - CONF
JO - Proceedings of the 5th International Conference on Software and Data Technologies - Volume 2: ICSOFT,
TI - MODEL CHECKING IS REFINEMENT - From Computation Tree Logic to Failure Trace Testing
SN - 978-989-8425-23-2
AU - D. Bruda S.
AU - Zhang Z.
PY - 2010
SP - 173
EP - 178
DO - 10.5220/0003006801730178