Abstract
This paper presents an extension of the tool JAG for verifying temporal properties expressed in LTL (Linear Temporal Logic) on B Event Systems. The tool generates a machine containing a B representation of the Büchi automaton associated with the LTL property to verify and includes it within the original B event system. Then, the user have to prove the consistency of the generated event system. This proof of consistency implies the satisfaction of the LTL property on the executions of the original event system.
Research partially founded by the french ACI Geccoo.
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
Abrial, J.-R.: The B Book. Cambridge University Press, Cambridge (1996)
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)
Giorgetti, A., Groslambert, J.: JAG: JML Annotation Generation for Verifying Temporal Properties. In: Baresi, L., Heckel, R. (eds.) FASE 2006 and ETAPS 2006. LNCS, vol. 3922, pp. 373–376. Springer, Heidelberg (2006)
Groslambert, J.: Verification of LTL on B event systems. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, Springer, Heidelberg (2006)
Pnueli, A.: The Temporal Logic of Program. In: 18th Ann. IEEE Symp. on foundations of computer science, pp. 46–57 (1977)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Groslambert, J. (2006). A JAG Extension for Verifying LTL Properties on B Event Systems. In: Julliand, J., Kouchnarenko, O. (eds) B 2007: Formal Specification and Development in B. B 2007. Lecture Notes in Computer Science, vol 4355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11955757_25
Download citation
DOI: https://doi.org/10.1007/11955757_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68760-3
Online ISBN: 978-3-540-68761-0
eBook Packages: Computer ScienceComputer Science (R0)