Abstract
We propose the nevertrace claim, which is a new construct for specifying the correctness properties that either finite or infinite execution traces (i.e., sequences of transitions) that should never occur. In semantics, it is neither similar to never claim and trace assertion, nor a simple combination of them. Furthermore, the theoretical foundation for checking nevertrace claims, namely the Asynchronous-Composition Büchi Automaton Control System (AC-BAC System), is proposed. The major contributions of the nevertrace claim include: a powerful construct for formalizing properties related to transitions and their labels, and a way for reducing the state space at the design stage.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Holzmann, G.J., Peled, D.: The state of SPIN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 385–389. Springer, Heidelberg (1996)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)
Ben-Ari, M.: Principles of the SPIN Model Checker. Springer, Heidelberg (2008)
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of the International Congress on Logic, Methodology, and Philosophy of Science, pp. 1–11. Stanford University Press, Stanford (1960)
Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science. Formal Models and Semantics, vol. B, pp. 133–191. Elsevier Science Publishers B.V, Amsterdam (1990)
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembinski, P., Sredniawa, M. (eds.) Proceedings of the 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, pp. 3–18. Chapman & Hall, Boca Raton (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, Z., Motet, G. (2010). Nevertrace Claims for Model Checking. In: van de Pol, J., Weber, M. (eds) Model Checking Software. SPIN 2010. Lecture Notes in Computer Science, vol 6349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16164-3_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-16164-3_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16163-6
Online ISBN: 978-3-642-16164-3
eBook Packages: Computer ScienceComputer Science (R0)