Using the ASTRAL model checker to analyze mobile IP

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Using the ASTRAL model checker to analyze mobile IP

Full text

Pdf (1.16 MB)

Source

International Conference on Software Engineering archive
Proceedings of the 21st international conference on Software engineering table of contents

Los Angeles, California, United States

Pages: 132 - 141

Year of Publication: 1999

ISBN:1-58113-074-0

Authors

Zhe Dang	Reliable Software Group, Computer Science Department, University of California, Santa Barbara, CA
Richard A. Kemmerer	Reliable Software Group, Computer Science Department, University of California, Santa Barbara, CA

Sponsors

IEEE-CS : Computer Society
IEEE-CS\TCSE : TC on Software Engineering
SIGADA: ACM Special Interest Group on Ada Programming Language
SIGSOFT: ACM Special Interest Group on Software Engineering
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 18, Citation Count: 7

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/302405.302459 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Hybrid specification of control systems, Proceedings of the 1st International Conference on Engineering of Complex Computer Systems, p.149, November 06-10, 1995
	2	G. Buonanno, A. Coen-Porisini, and W. Fornaciari, "Hardware specification using the assertion language ASTRAL," Proceedings of the Advanced Research Workshop on Correct Hardware Design Methodologies, Torino, Italy, June 1991.
	3	Alberto Coen-Porisini , Carlo Ghezzi , Richard A. Kemmerer, Specification of realtime systems using ASTRAL, IEEE Transactions on Software Engineering, v.23 n.9, p.572-598, September 1997 [doi>10.1109/32.629494]
	4	A. Coen-Porisini , R. A. Kemmerer , D. Mandrioli, A Formal Framework for ASTRAL Intralevel Proof Obligations, IEEE Transactions on Software Engineering, v.20 n.8, p.548-561, August 1994 [doi>10.1109/32.310665]
	5	Z. Dang and R. A. Kemmerer, "Using the ASTRAL model checker for cryptographic protocol analysis," Proceedings of the DIMACS Workshop on Design and Formal Verij?cation of Security Protocols, Rutgers University, 1997.
	6	Paul Z. Kolano , Zhe Dang , Richard A. Kemmerer, The design and analysis of real-time systems using the ASTRAL software development environment, Annals of Software Engineering, v.7 n.1-4, p.177-210, 1999 [doi>10.1023/A:1018934104631]
	7	Gavin Lowe , Bill Roscoe, Using CSP to Detect Errors in the TMN Protocol, IEEE Transactions on Software Engineering, v.23 n.10, p.659-669, October 1997 [doi>10.1109/32.637148]
	8	Peter J. McCann , Gruia-Catalin Roman, Modeling mobile IP in mobile UNITY, ACM Transactions on Software Engineering and Methodology (TOSEM), v.8 n.2, p.115-146, April 1999 [doi>10.1145/304399.304400]
	9	J. C. Mitchell , M. Mitchell , U. Stern, Automated analysis of cryptographic protocols using Mur/spl phi/, Proceedings of the 1997 IEEE Symposium on Security and Privacy, p.141, May 04-07, 1997
	10	Roger M. Needham , Michael D. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, v.21 n.12, p.993-999, Dec. 1978 [doi>10.1145/359657.359659]
	11	C. Perkins, "IP mobility support", Network Working Group Request for Comments: 2002, October 1996.
	12	Makoto Tatebayashi , Natsume Matsuzaki , David B. Newman, Jr., Key distribution protocol for digital mobile communication systems, Proceedings on Advances in cryptology, p.324-334, July 1989, Santa Barbara, California, United States

CITED BY 7

	Zhe Dang , Richard A. Kemmerer, Three approximation techniques for ASTRAL symbolic model checking of infinite state real-time systems, Proceedings of the 22nd international conference on Software engineering, p.345-354, June 04-11, 2000, Limerick, Ireland
	Premkumar T. Devanbu , Stuart Stubblebine, Software engineering for security: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.227-239, June 04-11, 2000, Limerick, Ireland
	John Penix , Willem Visser , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verification of time partitioning in the DEOS scheduler kernel, Proceedings of the 22nd international conference on Software engineering, p.488-497, June 04-11, 2000, Limerick, Ireland
	William Visser , SeungJoon Park , John Penix, Using predicate abstraction to reduce object-oriented programs for model checking, Proceedings of the third workshop on Formal methods in software practice, p.3-182, August 2000, Portland, Oregon, United States
	Zhe Dang , Oscar H. Ibarra , Richard A. Kemmerer, Generalized discrete timed automata: decidable approximations for safety verification, Theoretical Computer Science, v.296 n.1, p.59-74, 4 March 2003
	Richard A. Kemmerer, Cybersecurity, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
	John Penix , Willem Visser , Seungjoon Park , Corina Pasareanu , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verifying Time Partitioning in the DEOS Scheduling Kernel, Formal Methods in System Design, v.26 n.2, p.103-135, March 2005