DocumentCode
2416253
Title
Specification and verification of spatial data types with B-Toolkit
Author
Chun, Kim Yong ; Van Hung, Dang
Author_Institution
Int. Inst. for Software Technol., United Nations Univ., Macau
fYear
2002
fDate
2002
Firstpage
711
Lastpage
716
Abstract
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 by using abstract machine notations 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.
Keywords
abstract data types; formal specification; formal verification; software engineering; software tools; abstract machine notations; formal specification; formal verification; geometric structures; realm update operator; software development; spatial data types; Application software; Computer applications; Computer graphics; Formal specifications; Formal verification; Grid computing; Software systems; Solid modeling; Space technology; Spatial resolution;
fLanguage
English
Publisher
ieee
Conference_Titel
Computer Software and Applications Conference, 2002. COMPSAC 2002. Proceedings. 26th Annual International
ISSN
0730-3157
Print_ISBN
0-7695-1727-7
Type
conf
DOI
10.1109/CMPSAC.2002.1045085
Filename
1045085
Link To Document