Modelling and verification of Biphase Mark Protocols in Duration Calculus using PVS

Author

Van Hung, Dang

Author_Institution

Int. Inst. for Software Technol., United Nations Univ., Macau

fYear

1998

fDate

23-26 Mar 1998

Firstpage

88

Lastpage

98

Abstract

The paper presents a model of Biphase Mark Protocols (BMP) using Duration Calculus, which seems to be more general and more intuitive than the others in the literature (J.S. Moore, 1994). With Duration Calculus we can model the behaviour of the bus in a natural way and in more detail. The model makes it possible to specify and verify BMP using PVS/DC^- tool (Mao Xiaoguang et al., 1996). The mechanical verification not only ensures the correctness of the protocol, but also helps engineers to choose the optimal values for the parameters given the ratio between the clock rates of the sender and the receiver and the time for changing the signal from high to low and low to high

Keywords

Boolean functions; formal verification; process algebra; protocols; real-time systems; theorem proving; BMP; Biphase Mark Protocols; Duration Calculus; PVS/DC^- tool; bus behaviour; clock rates; formal methods; mechanical verification; protocol correctness; real time systems; Boolean functions; Calculus; Clocks; Decoding; Information technology; Paper technology; Physical layer; Protocols; Real time systems;

fLanguage

English

Publisher

ieee

Conference_Titel

Application of Concurrency to System Design, 1998. Proceedings., 1998 International Conference on

Conference_Location

Fukushima

Print_ISBN

0-8186-8350-3

Type

conf

DOI

10.1109/CSD.1998.657542

Filename

657542