loading...
Specification and Verification of Spatial Data Types with B-Toolkit
Oxford, England August 26-August 29
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CMPSAC.2002.104508526th Annual International Computer So ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
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
Usage of this product signifies your acceptance of the Terms of Use.