Abstract
Refinement is the best established method to verify complex models using proof-theoretic techniques. One of the challenge of applying this method, besides the tediousness of the proofs, is the slow feedback in assessing the adequacy of the models. In this paper, we show how the tool SPIN has been used to help with formal proofs of a hierarchy of models specified in TLA+. Without being a substitute for a formal proof, using SPIN in this context can reduce the workload by providing a means to quickly assess models, invariants and refinement mappings.
We use the term reachability analysis in the sense of Holzmann [7].
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Martin Abadi and Stephan Merz. On TLA as a logic. In Manfred Broy, editor, Deductive Program Design, pages 235–271. NATO ASI Series, Springer-Verlag, 1995.
J.-R. Abrial. The B Book: Assigning Programs to Meanings. Cambridge University Press, 1996.
J. Hajek. Automatically verified data transfer protocols. In 4th ICCC pages 749–756, 1978.
Klaus Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe FME '96, number 1051 in Lecture Notes in Computer Science, pages 662–681, Oxford, UK, March 1996. Springer-Verlag.
P. Herrmann and H. Krumm. Re-usable verification elements for high-speed transfer protocol configu ration. In Protocol Specification, Testing and Verification XV, pages 171–186. Chapman & Hall, 1995.
Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
Gerard J. Holzmann and Doron Peled. An improvement in formal verification. In Dieter Hogrefe and Stefan Leue, editors, 7th Int. Conf. on Formal Description Techniques. Chapman and Hall, 1994.
Peter Ladkin. Formal but lively buffers in TLA+. Technical report, Universität von Bielefeld, 1996. from http://www.rvs.uni-bielefeld.de/.
Leslie Lamport. The temporal logic of actions. ACM TOPLAS, 16(3):872–923, 1994.
Leslie Lamport. TLA+. Technical report, DEC-SRC, 1995. from http://www.research.digital.com/SRC/personal/Leslie-Lamport/tla/papers.html.
Zoar Manna and Amir Pnueli. A Temporal Proof Methodology for Reactive Systems. In Program Design Calculi, NATO ASI Series, Series F. Springer Verlag, 1993.
Natarajan and G.J. Holzmann. Towards a formal semantics of PROMELA. In Proceedings of the 2nd SPIN Workshop, 1996.
S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification of fault-tolerant architectures: Prolegmena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grégoire, J.C. (1997). TLA + PROMELA: Conjecture, check, proof. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds) FME '97: Industrial Applications and Strengthened Foundations of Formal Methods. FME 1997. Lecture Notes in Computer Science, vol 1313. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63533-5_20
Download citation
DOI: https://doi.org/10.1007/3-540-63533-5_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63533-8
Online ISBN: 978-3-540-69593-6
eBook Packages: Springer Book Archive