Formal specification of a real-time lift dispatching system

Author

Wang, Yingxu ; Ngolah, Foinjong C.

Author_Institution

Dept of Electr. & Comput. Eng., Calgary Univ., Alta., Canada

Volume

2

fYear

2002

fDate

6/24/1905 12:00:00 AM

Firstpage

669

Abstract

This paper describes the formal specification of a lift dispatching system (LDS) by the real-time process algebra (RTPA). It is recognized that the specification of a real-time system is a hard problem because the specification has to address the 3D behaviors of software where timing, logic and dynamic memory allocation functionalities are very critical. The real-time process algebra (RTPA) is a descriptive formal notation system designed for real-time software system specification, and is able to address the 3D properties of real-time software systems. The aim of this paper is to demonstrate the use of RTPA in describing a lift dispatching system (LDS). The case study on LDS illustrates the applications of RTPA in real-time system specification and refinement. This case study on the realtime LDS system shows the features and advantages of the algebra-based approach to real-time system specification and refinement in RTPA.

Keywords

control engineering computing; dispatching; formal specification; lifts; process algebra; real-time systems; timing; 3D behaviors; descriptive formal notation system; dynamic memory allocation; formal specification; logic; real-time lift dispatching system; real-time process algebra; refinement; timing; Algebra; Computer interfaces; Control systems; Dispatching; Drives; Formal specifications; Hardware; Real time systems; Software systems; Timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Electrical and Computer Engineering, 2002. IEEE CCECE 2002. Canadian Conference on

ISSN

0840-7789

Print_ISBN

0-7803-7514-9

Type

conf

DOI

10.1109/CCECE.2002.1013021

Filename

1013021