Search

A home care plan (HCP) can be integrated with an electronic medical records (EMR) system, serving as an example of a real-time system with concurrent processes. To ensure effective operation, HCPs must be free of software bugs. In this paper, we explore the modeling and verification of HCPs from the perspective of scheduling data operationalization. Specifically, we investigate how patients can obtain home services while preventing scheduling conflicts in the context of limited resources. Our goal is to develop and verify robust models for this purpose. We employ formalism to construct and validate the model, following these steps: i) develop requirements and specifications; ii) create a model with concurrent processes using timed automata; and iii) verify the model using UPPAAL tools. Our study focuses on HCP implementation at a regional general hospital in Banyumas District, Central Java, Indonesia. The results include models and specifications based on timed automata and timed computation tree logic (TCTL). We successfully verified a concurrent model that utilizes synchronized counter variables and a sender-receiver approach to analyze collision constraints arising from the synchronization of patient and resource plans. [ABSTRACT FROM AUTHOR]

This article, published in the Turkish Journal of Mathematics, explores the topic of interpolation polynomials associated with linear recurrences. The authors investigate the use of polynomial interpolation using basic points given by (t, Gt) for a linear recurrence (Gn). They develop formulas related to finite differences and provide an explicit formula for the interpolation polynomials. The article also includes introductory information on finite differences and properties of recursive sequences. The authors provide examples and demonstrate the application of their approach in obtaining interpolation polynomials. The research was supported by multiple grants. [Extracted from the article]