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
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;
Conference_Titel :
Information Engineering and Computer Science, 2009. ICIECS 2009. International Conference on
Conference_Location :
Wuhan
Print_ISBN :
978-1-4244-4994-1
DOI :
10.1109/ICIECS.2009.5363595
