{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T15:06:07Z","timestamp":1781103967717,"version":"3.54.1"},"reference-count":23,"publisher":"IGI Global Scientific Publishing","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009,10,1]]},"abstract":"<p>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.<\/p>","DOI":"10.4018\/jssci.2009062506","type":"journal-article","created":{"date-parts":[[2010,4,30]],"date-time":"2010-04-30T08:46:33Z","timestamp":1272617193000},"page":"111-137","source":"Crossref","is-referenced-by-count":21,"title":["The Formal Design Model of a Lift Dispatching System (LDS)"],"prefix":"10.4018","volume":"1","author":[{"given":"Yingxu","family":"Wang","sequence":"first","affiliation":[{"name":"University of Calgary, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cyprian F.","family":"Ngolah","sequence":"additional","affiliation":[{"name":"University of Calgary, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hadi","family":"Ahmadi","sequence":"additional","affiliation":[{"name":"University of Calgary, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philip","family":"Sheu","sequence":"additional","affiliation":[{"name":"Wuhan University, China and University of California-Irvine, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shi","family":"Ying","sequence":"additional","affiliation":[{"name":"Wuhan University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"2432","reference":[{"key":"jssci.2009062506-0","unstructured":"Bjorner, D., & Jones, C. B. (1982). Formal Specification and Software Development. Prentice Hall."},{"key":"jssci.2009062506-1","first-page":"48","article-title":"New Approach in the Development of Elevator Group Control Algorithms. Amsterdam.","volume":"4","author":"P.Chenais","year":"1992","journal-title":"ELEVCON"},{"key":"jssci.2009062506-2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00365335"},{"key":"jssci.2009062506-3","unstructured":"Hamdi, M., Mulvaney, D.J., & Sillitoe, I.P. (1995). An Intelligent Real-time Lift Scheduling System. Workshop of the UK Planning and Scheduling Special Interest Group, 14."},{"key":"jssci.2009062506-4","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.232191"},{"key":"jssci.2009062506-5","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"jssci.2009062506-6","unstructured":"Hoare, C. A. R. (1985). Communicating Sequential Processes. Prentice-Hall Inc."},{"key":"jssci.2009062506-7","unstructured":"Liu, J. (2000). Real-Time Systems. Upper Saddle River, NJ: Prentice Hall."},{"key":"jssci.2009062506-8","unstructured":"McDermid, J. A. (1991). Software Engineer\u2019s Reference Book. Oxford, UK: Butterworth-Heinemann Ltd."},{"issue":"4","key":"jssci.2009062506-9","first-page":"237","article-title":"The Real-Time Task Scheduling Algorithm of RTOS+.","volume":"29","author":"C. F.Ngolah","year":"2004","journal-title":"IEEE Canadian Journal of Electrical and Computer Engineering"},{"key":"jssci.2009062506-10","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020561826073"},{"key":"jssci.2009062506-11","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025457612549"},{"key":"jssci.2009062506-12","doi-asserted-by":"crossref","unstructured":"Wang, Y. (2007, July). Software Engineering Foundations: A Software Science Perspective. CRC Series in Software Engineering (Vol. II). Auerbach Publications, USA.","DOI":"10.1201\/9780203496091.pt3"},{"issue":"2","key":"jssci.2009062506-13","doi-asserted-by":"crossref","first-page":"44","DOI":"10.4018\/jcini.2008040103","article-title":"RTPA: A Denotational Mathematics for Manipulating Intelligent and Computational Behaviors.","volume":"2","author":"Y.Wang","year":"2008","journal-title":"International Journal of Cognitive Informatics and Natural Intelligence"},{"issue":"2","key":"jssci.2009062506-14","doi-asserted-by":"crossref","first-page":"95","DOI":"10.4018\/jcini.2008040106","article-title":"Deductive Semantics of RTPA.","volume":"2","author":"Y.Wang","year":"2008","journal-title":"International Journal of Cognitive Informatics and Natural Intelligence"},{"key":"jssci.2009062506-15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87563-5_4"},{"key":"jssci.2009062506-16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87563-5_2"},{"issue":"3","key":"jssci.2009062506-17","doi-asserted-by":"crossref","DOI":"10.4018\/jssci.2009070107","article-title":"The Formal Design Model of a Telephone Switching System (TSS).","volume":"1","author":"Y.Wang","year":"2009","journal-title":"International Journal of Software Science and Computational Intelligence"},{"key":"jssci.2009062506-18","doi-asserted-by":"crossref","unstructured":"Wang, Y., & King, G. (2000). Software Engineering Processes: Principles and Applications. CRC Series in Software Engineering (Vol. I). CRC Press, USA.","DOI":"10.1201\/9781482274547"},{"key":"jssci.2009062506-19","doi-asserted-by":"publisher","DOI":"10.1145\/351936.351943"},{"key":"jssci.2009062506-20","unstructured":"Wang, Y., & Noglah, C. F. (2002, May). Formal Specification of a Real-Time Lift Dispatching System. Proc. 2002 IEEE Canadian Conference on Electrical and Computer Engineering (CCECE'02) (pp. 669-674). Winnipeg, Manitoba, Canada."},{"issue":"2","key":"jssci.2009062506-21","doi-asserted-by":"crossref","first-page":"73","DOI":"10.4018\/jcini.2007040105","article-title":"The Cognitive Process of Decision Making.","volume":"1","author":"Y.Wang","year":"2007","journal-title":"International Journal of Cognitive Informatics and Natural Intelligence"},{"key":"jssci.2009062506-22","unstructured":"Wang, Y., & Zhang, Y. (2003, May). Formal Description of an ATM System by RTPA. Proc. 16th Canadian Conference on Electrical and Computer Engineering (CCECE'03) (pp. 1255-1258). Montreal, Canada: IEEE CS Press."}],"container-title":["International Journal of Software Science and Computational Intelligence"],"original-title":[],"language":"ng","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=37491","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T13:15:39Z","timestamp":1654089339000},"score":1,"resource":{"primary":{"URL":"https:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/jssci.2009062506"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2009,10,1]]},"references-count":23,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,10]]}},"URL":"https:\/\/doi.org\/10.4018\/jssci.2009062506","relation":{},"ISSN":["1942-9045","1942-9037"],"issn-type":[{"value":"1942-9045","type":"print"},{"value":"1942-9037","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,10,1]]}}}