DocumentCode
2821315
Title
Integrating the B-Method into PVS
Author
Zhou, J.M. ; Guo, Jian ; Song, Fu
Author_Institution
Software Eng. Inst., East China Normal Univ., Shanghai, China
fYear
2009
fDate
19-20 Dec. 2009
Firstpage
1
Lastpage
4
Abstract
This paper presents a method that can translate a system described by B-method into formal specification language of PVS. In this method, a machine in B-method is expressed to be a theory in PVS, while an invariant to be a type in PVS. Some properties described by B-method are transformed into conjectures of PVS language, then these conjectures can be proved effectively by PVS prover. In the end, an example, a lift system controller, is given to illustrate an application of this method.
Keywords
formal languages; specification languages; theorem proving; B-method; PVS prover; PVS theory; formal specification language; lift system controller; Control systems; Displays; Formal specifications; Hardware; Information technology; Logic; Safety; Software engineering; Software quality; Specification languages;
fLanguage
English
Publisher
ieee
Conference_Titel
Information Engineering and Computer Science, 2009. ICIECS 2009. International Conference on
Conference_Location
Wuhan
Print_ISBN
978-1-4244-4994-1
Type
conf
DOI
10.1109/ICIECS.2009.5363595
Filename
5363595
Link To Document