We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
The Formal Design Model of a Lift Dispatching System (LDS).
- Authors
Yingxu Wang; Ngolah, Cyprian F.; Ahmadi, Hadi; Philip Sheu; Shi Ying
- Abstract
A Lift Dispatching System (LDS) is a typical real-time system that is highly complicated in design and implementation. This article presents the formal design, specification, and modeling of the LDS system using a denotational mathematics known as Real-Time Process Algebra (RTPA). The conceptual model of the LDS system is introduced as the initial requirements for the system. The architectural model of the LDS system is created using RTPA architectural modeling methodologies and refined by a set of Unified Data Models (UDMs). The static behaviors of the LDS system are specified and refined by a set of Unified Process Models (UPMs) for the lift dispatching and serving processes. The dynamic behaviors of the LDS system are specified and refined by process priority allocation and process deployment models. Based on the formal design models of the LDS system, code can be automatically generated using the RTPA Code Generator (RTPA-CG), or be seamlessly transferred into programs by programmers. The formal models of LDS may not only serve as a formal design paradigm of real-time software systems, but also a test bench of the expressive power and modeling capability of exiting formal methods in software engineering.
- Publication
International Journal of Software Science & Computational Intelligence, 2009, Vol 1, Issue 4, p111
- ISSN
1942-9045
- Publication type
Article
- DOI
10.4018/jssci.2009062506