{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T15:07:26Z","timestamp":1781104046045,"version":"3.54.1"},"reference-count":40,"publisher":"IGI Global Scientific Publishing","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,4,1]]},"abstract":"<p>A real-time operating system (RTOS) provides a platform for the design and implementation of a wide range of applications in real-time systems, embedded systems, and mission-critical systems. This paper presents a formal design model for a general RTOS known as RTOS+ that enables a specific target RTOS to be rigorously and efficiently derived in real-world applications. The methodology of a denotational mathematics, Real-Time Process Algebra (RTPA), is described for formally modeling and refining architectures, static behaviors, and dynamic behaviors of RTOS+. The conceptual model of the RTOS+ system is introduced as the initial requirements for the system. The architectural model of RTOS+ is created using RTPA architectural modeling methodologies and refined by a set of Unified Data Models (UDMs). The static behaviors of RTOS+ are specified and refined by a set of Unified Process Models (UPMs). The dynamic behaviors of the RTOS+ system are specified and refined by the real-time process scheduler and system dispatcher. This work is presented in two papers; the conceptual and architectural models of RTOS+ is described in this paper, while the static and dynamic behavioral models of RTOS+ will be elaborated in a forthcoming paper.<\/p>","DOI":"10.4018\/jssci.2010040106","type":"journal-article","created":{"date-parts":[[2010,6,30]],"date-time":"2010-06-30T17:08:42Z","timestamp":1277917722000},"page":"105-122","source":"Crossref","is-referenced-by-count":20,"title":["The Formal Design Model of a Real-Time Operating System (RTOS+)"],"prefix":"10.4018","volume":"2","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":"Sentinel Trending & Diagnostics Ltd., Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guangping","family":"Zeng","sequence":"additional","affiliation":[{"name":"University of Science and Technology Beijing, China and University of California, Berkeley,USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philip C.Y.","family":"Sheu","sequence":"additional","affiliation":[{"name":"Wuhan University, China and University of California, Irvine, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C. Philip","family":"Choy","sequence":"additional","affiliation":[{"name":"University of Calgary, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yousheng","family":"Tian","sequence":"additional","affiliation":[{"name":"University of Calgary, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"2432","reference":[{"key":"jssci.2010040106-0","doi-asserted-by":"publisher","DOI":"10.1109\/12.40843"},{"key":"jssci.2010040106-1","author":"G.Bollella","year":"2002","journal-title":"The Real-Time Specification for Java"},{"key":"jssci.2010040106-2","doi-asserted-by":"crossref","unstructured":"Brinch-Hansen, P. (1971, October). Short-Term Scheduling in Multiprogramming Systems. In Proceedings of the Third ACM Symposium on Operating Systems Principles (pp. 103-105).","DOI":"10.1145\/800212.806506"},{"key":"jssci.2010040106-3","author":"H. M.Deitel","year":"1992","journal-title":"The Design of OS\/2"},{"key":"jssci.2010040106-4","doi-asserted-by":"publisher","DOI":"10.1145\/363095.363143"},{"key":"jssci.2010040106-5","unstructured":"ETTX. (2009, February). In Proceedings of the First Eueopean TinyOS Technology Exchange, Cork, Ireland."},{"key":"jssci.2010040106-6","doi-asserted-by":"crossref","unstructured":"Ford, B., Back, G., Benson, G., Lepreau, J., Lin, A., & Shivers, O. (1997). The Flux OSKit: a Substrate for OS and Language Research. In Proceedings of the 16th ACM Symposium on Operating Systems Principles, Saint Malo, France.","DOI":"10.1145\/268998.266642"},{"key":"jssci.2010040106-7","unstructured":"ISO\/IEC 9945-1. (1996). ISO\/IEC Standard 9945-1: Information Technology-Portable Operating System Interface (POSIX) - Part 1: System Application Program Interface (API) (C Language). ISO\/IEC."},{"key":"jssci.2010040106-8","author":"J.Kreuzinger","year":"2002","journal-title":"Real-Time Event Handling and Scheduling on a Multithread Java Microntroller"},{"key":"jssci.2010040106-9","author":"J. J.Labrosse","year":"1999","journal-title":"MicroC\/OS-II, The Real-Time Kernel"},{"key":"jssci.2010040106-10","author":"E. L.Lamie","year":"2008","journal-title":"Real-Time Embedded Multithreading using ThreadX and MIPS"},{"key":"jssci.2010040106-11","author":"P. A.Laplante","year":"1977","journal-title":"Real-Time Systems Design and Analysis"},{"key":"jssci.2010040106-12","author":"B.Lewis","year":"1998","journal-title":"Multithreaded Programming with Pthreads"},{"issue":"1","key":"jssci.2010040106-13","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1145\/321738.321743","article-title":"Scheduling Algorithms for Multiprogramming in Hard-Real-Time Environments.","volume":"20","author":"C.Liu","year":"1973","journal-title":"Journal of the Association for Computing Machinery"},{"key":"jssci.2010040106-14","author":"J.McDermid","year":"1991","journal-title":"Software Engineer\u2019s Reference Book"},{"issue":"3","key":"jssci.2010040106-15","first-page":"71","article-title":"Tool Support for Software Development based on Formal Specifications in RTPA.","volume":"3","author":"C. F.Ngolah","year":"2009","journal-title":"International Journal of Software Engineering and Its Applications"},{"issue":"4","key":"jssci.2010040106-16","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.2010040106-17","author":"J. L.Peterson","year":"1985","journal-title":"Operating System Concepts"},{"key":"jssci.2010040106-18","doi-asserted-by":"crossref","unstructured":"Rivas, M. A., & Harbour, M. G. (2001, May). MaRTE OS: An Ada Kernel for Real-Time Embedded Applications. In Proceedings of Ada-Europe 2001, Leuven, Belgium.","DOI":"10.1007\/3-540-45136-6_24"},{"key":"jssci.2010040106-19","doi-asserted-by":"publisher","DOI":"10.1109\/12.57058"},{"key":"jssci.2010040106-20","author":"A.Silberschatz","year":"2003","journal-title":"Applied Operating System Concepts"},{"key":"jssci.2010040106-21","author":"A. S.Tanenbaum","year":"1994","journal-title":"Distributed Operating Systems"},{"key":"jssci.2010040106-22","author":"P. G.Viscarola","year":"2001","journal-title":"Windows NT Device Driver Development"},{"key":"jssci.2010040106-23","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020561826073"},{"key":"jssci.2010040106-24","doi-asserted-by":"crossref","DOI":"10.1201\/9781420039870.ch144","article-title":"Operating Systems","author":"Y.Wang","year":"2004","journal-title":"The Engineering Handbook"},{"key":"jssci.2010040106-25","doi-asserted-by":"crossref","unstructured":"Wang, Y. (2007). Software Engineering Foundations: A Software Science Perspective (CRC Series in Software Engineering, Vol. 2). Boston: Auerbach Publications.","DOI":"10.1201\/9780203496091.pt3"},{"issue":"2","key":"jssci.2010040106-26","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"},{"key":"jssci.2010040106-27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87563-5_4"},{"issue":"2","key":"jssci.2010040106-28","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.2010040106-29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87563-5_2"},{"issue":"3","key":"jssci.2010040106-30","doi-asserted-by":"crossref","first-page":"282","DOI":"10.3233\/FI-2009-0019","article-title":"Paradigms of Denotational Mathematics for Cognitive Informatics and Cognitive Computing.","volume":"90","author":"Y.Wang","year":"2009","journal-title":"Fundamenta Informaticae"},{"issue":"3","key":"jssci.2010040106-31","doi-asserted-by":"crossref","first-page":"92","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.2010040106-32","doi-asserted-by":"publisher","DOI":"10.1016\/j.cogsys.2008.08.003"},{"issue":"1","key":"jssci.2010040106-33","doi-asserted-by":"crossref","first-page":"100","DOI":"10.4018\/jcini.2008010108","article-title":"Formal Modeling and Specification of Design Patterns Using RTPA.","volume":"2","author":"Y.Wang","year":"2008","journal-title":"International Journal of Cognitive Informatics and Natural Intelligence"},{"issue":"4","key":"jssci.2010040106-34","doi-asserted-by":"crossref","first-page":"98","DOI":"10.4018\/jssci.2009062506","article-title":"The Formal Design Model of a Lift Dispatching System (LDS).","volume":"1","author":"Y.Wang","year":"2009","journal-title":"International Journal of Software Science and Computational Intelligence"},{"issue":"2","key":"jssci.2010040106-35","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"},{"issue":"2","key":"jssci.2010040106-36","doi-asserted-by":"crossref","DOI":"10.4018\/jssci.2010040103","article-title":"Design and Implementation of an Autonomic Code Generator based on RTPA.","volume":"2","author":"Y.Wang","year":"2010","journal-title":"International Journal of Software Science and Computational Intelligence"},{"key":"jssci.2010040106-37","article-title":"The Formal Design Model of a Real-Time Operating System (RTOS+): Static and Dynamic Behavior Models.","author":"Y.Wang","journal-title":"International Journal of Software Science and Computational Intelligence"},{"issue":"1","key":"jssci.2010040106-38","doi-asserted-by":"crossref","first-page":"102","DOI":"10.4018\/jssci.2010101907","article-title":"The Formal Design Models of an Automatic Teller Machine (ATM).","volume":"2","author":"Y.Wang","year":"2010","journal-title":"International Journal of Software Science and Computational Intelligence"},{"key":"jssci.2010040106-39","unstructured":"Yodaiken, V. (1999, May). An RT-Linux Manifesto. In Proceedings of the 5th Linux Expo, Raleigh, NC."}],"container-title":["International Journal of Software Science and Computational Intelligence"],"original-title":[],"language":"ng","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=43900","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,2]],"date-time":"2022-06-02T01:10:47Z","timestamp":1654132247000},"score":1,"resource":{"primary":{"URL":"https:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/jssci.2010040106"}},"subtitle":["Conceptual and Architectural Frameworks"],"short-title":[],"issued":{"date-parts":[[2010,4,1]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,4]]}},"URL":"https:\/\/doi.org\/10.4018\/jssci.2010040106","relation":{},"ISSN":["1942-9045","1942-9037"],"issn-type":[{"value":"1942-9045","type":"print"},{"value":"1942-9037","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,4,1]]}}}