An approach to verifying concurrent systems-a medical information bus (MIB) case study

Author

Curran, Phil ; Norrie, Kathy

Author_Institution

R. Free Hospital Sch. of Med., London Univ., UK

fYear

1992

fDate

14-17 Jun 1992

Firstpage

74

Lastpage

83

Abstract

An automated method for verifying aspects of the data link communications protocol for the proposed IEEE P1073 Standard for Medical Device Communications is described. This protocol is specified using the formal description technique LOTOS, and the specification and an associated verification are implemented in the Larch Theorem Prover. The advantages of this approach for the design and verification of large and complex systems are discussed

Keywords

formal specification; medical computing; program verification; protocols; standards; IEEE P1073 Standard; LOTOS; Larch Theorem Prover; Medical Device Communications; concurrent systems; data link communications protocol; formal description technique; medical information bus; specification; verification; Biomedical imaging; Communication standards; Communication system control; Computer aided software engineering; Computer networks; ISO standards; LAN interconnection; Local area networks; Open systems; Protocols;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer-Based Medical Systems, 1992. Proceedings., Fifth Annual IEEE Symposium on

Conference_Location

Durham, NC

Print_ISBN

0-8186-2742-5

Type

conf

DOI

10.1109/CBMS.1992.244961

Filename

244961