Specification and Verification of Spatial Data Types with B-Toolkit

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Kim Yong Chun Articles by Dang Van Hung

26th Annual International Computer Software and Applications Conference

Oxford, England

August 26-August 29

ISBN: 0-7695-1727-7

	ASCII Text	x
	Kim Yong Chun, Dang Van Hung, "Specification and Verification of Spatial Data Types with B-Toolkit," Computer Software and Applications Conference, Annual International, pp. 711, 26th Annual International Computer Software and Applications Conference, 2002.

	BibTex	x
	@article{ 10.1109/CMPSAC.2002.1045085, author = {Kim Yong Chun and Dang Van Hung}, title = {Specification and Verification of Spatial Data Types with B-Toolkit}, journal ={Computer Software and Applications Conference, Annual International}, volume = {0}, year = {2002}, issn = {0730-3157}, pages = {711}, doi = {http://doi.ieeecomputersociety.org/10.1109/CMPSAC.2002.1045085}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Computer Software and Applications Conference, Annual International TI - Specification and Verification of Spatial Data Types with B-Toolkit SN - 0730-3157 SP EP A1 - Kim Yong Chun, A1 - Dang Van Hung, PY - 2002 KW - null VL - 0 JA - Computer Software and Applications Conference, Annual International ER -

Kim Yong Chun, United Nations University

Dang Van Hung, United Nations University

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CMPSAC.2002.1045085

Spatial data types provide a fundamental abstraction for modelling the geometric structures of objects in space, their relationships, properties and operations. In this work, we present a formal specification and verification of spatial data types with the B-Toolkit. We give a formal specification of a realm and operations over it using Abstract Machine Notations (AMN) of B. We then refine and implement a realm update operator in B, and verify formally an implementation of a realm update operator with B-Toolkit.

Citation:

Kim Yong Chun, Dang Van Hung, "Specification and Verification of Spatial Data Types with B-Toolkit," compsac, pp.711, 26th Annual International Computer Software and Applications Conference, 2002

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.