Abstract
This paper presents a formalization of finite and infinite sequences in domain theory carried out in the theorem prover Isabelle. The results are used to model the metatheory of I/O automata; they are, however, applicable to any trace based model of parallelism which distinguishes internal and external actions. We make use of the logic HOLCF, an extension of HOL with domain theory and show how to move between HOL and HOLCF. This allows us to restrict the use of HOLCF to metatheoretic arguments while actual refinement proofs between I/O automata are carried out within the simpler logic HOL. In order to evaluate the formalization we prove the correctness of a generalized refinement concept in I/O automata.
Research supported by BMBF, KorSys.
Research supported by ESPRIT BRA 6453, Types.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Abadi and L. Lamport. The existence of refinement mappings. In Proc. 3rd IEEE Symp. LICS, pages 165–177. IEEE Computer Society Press, 1988.
S. Brooks. Pull abstraction for a shared variable parallel language. In Proc. 8th IEEE Symp. Logic in Computer Science, pages 98–109, 1993.
C.-T. Chou and D. Peled. Formal verification of a partial-order reduction technique for model checking. In T. Margaria and B. Steffen, editors, Proc. 2nd TACAS, volume 1055 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
I. P. D.J.B. Bosscher and F. Vaandrager. Verification of an audio control protocol. In W. d. R. H. Langmaack and J. Vytopil, editors, Proc. 3rd Int. School and Symposium FTRTFT'94, volume 863 of Lecture Notes in Computer Science, pages 170–192. Springer, 1994.
S. Feferman. Computation on abstract data types. the extensional approach, with an application to streams. Annals of Pure and Applied Logic, 81:75–113, 1996.
R. Gawlick, R. Segala, J. Sogaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. Technical Report MIT/LCS/TR-587, Laboratory for Computer Science, MIT, Cambridge, MA., 1993. Extended abstract in Proceedings ICALP'94.
M. Gordon and T. Melham. Introduction to HOL: a theorem-proving environment for higher-order logic. Cambridge University Press, 1993.
P. Loewenstein. A formal theory of simulations between infinite automata. Formal Methods in System Design, 3(1):117–149, 1993.
V. Luchangco, E. Söylemez, S. Garland, and N. Lynch. Verifying timing properties of concurrent algorithms. In Proc. 7th Int. Conf. Formal Description Techniques, pages 259–273. IFIP WG6.1, Chapman and Hall, 1994.
N. Lynch and M. Tuttle. An introduction to Input/Output automata. CWI Quarterly, 2(3):219–246, 1989.
N. Lynch and F. Vaandrager. Forward and backward simulations — part I: Untimed systems. Information and Computation, 121(2):214–233, 1995.
O. Müller and T. Nipkow. Combining model checking and deduction for I/O-automata. In Proc. 1st Workshop Tools and Algorithms for the Construction and Analysis of Systems, volume 1019 of Lecture Notes in Computer Science, pages 1–16. Springer-Verlag, 1995.
T. Nipkow and K. Slind. I/O automata in Isabelle/HOL. In P. Dybjer, B. Nordström, and J. Smith, editors, Types for Proofs and Programs, volume 996 of Lecture Notes in Computer Science, pages 101–119. Springer-Verlag, 1995.
D. v. Oheimb. Datentypspezifikationen in Higher-Order LCF. Master's thesis, Computer Science Department, Technical University Munich, 1995.
L. Paulson. Co-induction and co-recursion in higher-order logic. Technical Report TR-334, Univ. of Cambridge, Computer Lab., 1994.
L. C. Paulson. Logic and Computation. Cambridge University Press, 1987.
L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.
F. Regensburger. HOLCF: Higher Order Logic of Computable Functions. In E. Schubert, P. Windley, and J. Alves-Foss, editors, Higher Order Logic Theorem Proving and its Applications, volume 971 of Lecture Notes in Computer Science, pages 293–307. Springer-Verlag, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Müller, O., Nipkow, T. (1997). Traces of I/O-automata in Isabelle/HOLCF. In: Bidoit, M., Dauchet, M. (eds) TAPSOFT '97: Theory and Practice of Software Development. CAAP 1997. Lecture Notes in Computer Science, vol 1214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030627
Download citation
DOI: https://doi.org/10.1007/BFb0030627
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62781-4
Online ISBN: 978-3-540-68517-3
eBook Packages: Springer Book Archive