Claim Missing Document
Check
Articles

Found 3 Documents
Search

Timed concurrent system modeling and verification of home care plan Taryana, Acep; Adzkiya, Dieky; Mufid, Muhammad Syifa'ul; Mukhlash, Imam
International Journal of Electrical and Computer Engineering (IJECE) Vol 15, No 1: February 2025
Publisher : Institute of Advanced Engineering and Science

Show Abstract | Download Original | Original Source | Check in Google Scholar | DOI: 10.11591/ijece.v15i1.pp870-882

Abstract

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.
Peningkatan Kapabilitas Guru dan Siswa SMA di Yayasan Pendidikan Pesantren Zainul Hasan Genggong untuk Menghadapi Olimpiade Sains Kabupaten (OSK) bidang Matematika dan Informatika di Kabupaten Probolinggo Fahim, Kistosil; Subiono, Subiono; Imron, Chairul; Herisman, Iis; Usadha, I Gst Ngr Rai; Soleha, Soleha; Mufid, Muhammad Syifa'ul
Sewagati Vol 9 No 1 (2025)
Publisher : Pusat Publikasi ITS

Show Abstract | Download Original | Original Source | Check in Google Scholar | DOI: 10.12962/j26139960.v9i1.2257

Abstract

Pelatihan yang diadakan untuk guru matematika dan siswa SMA di Yayasan Pendidikan Pesantren Zainul Hasan Genggong (PPZHG) bertujuan memperdalam pemahaman konsep-konsep mata pelajaran Matematika, dengan fokus khusus pada bagaimana guru dan siswa mampu menyelesaikan soal-soal Olimpiade Sains Kabupaten (OSK) di bidang Matematika dan Informatika. Program pelatihan ini dilaksanakan secara luring sesuai dengan jadwal yang telah disusun oleh yayasan. Hasil pelatihan menunjukkan bahwa 1) para guru mampu menyalurkan materi yang mereka terima kepada murid-muridnya, dan 2) siswa yang mengikuti pelatihan dapat berbagi ilmu dengan teman sebayanya serta adik-adik kelas mereka. Sasaran utama dari kegiatan ini adalah meningkatkan kemampuan peserta dalam menyelesaikan soal-soal OSK Matematika dan Informatika, yang ditunjukkan melalui hasil post-test yang lebih baik dibandingkan dengan pre-test.
Identify Solutions to Systems of Linear Latin for Square Equations over Maxmin-ω 'Azizah, Nilatul; Mufid, Muhammad Syifa'ul
Jambura Journal of Mathematics Vol 7, No 1: February 2025
Publisher : Department of Mathematics, Universitas Negeri Gorontalo

Show Abstract | Download Original | Original Source | Check in Google Scholar | DOI: 10.37905/jjom.v7i1.30278

Abstract

Maxmin-\omega algebra is a mathematical system that generalizes maxmin algebra by introducing the parameter \omega (0 \omega \leq 1), which regulates the algebraic operations to enhance its applicability in optimization and decision-making processes. When \omega=1, the system corresponds to the max operation, whereas for \omega approaching 0, it behaves like the min operation. This research investigates the solution characteristics of a linear equation system in maxmin-\omega algebra, specifically A \otimes_{\omega} \textbf{x} = \textbf{b}, where A is a Latin square matrix. Understanding these solutions is crucial for determining the conditions of existence and uniqueness, which will ultimately influence the development of more efficient solution methods for various applications. Furthermore, the study analyzes the impact of the value of \omega and the matrix permutation structure on the solutions of the system. This study employs an analytical approach utilizing maxmin-\omega algebra theory to determine solution existence and assess the impact of \omega variations in linear equations with Latin square matrices. The results reveal that the solution existence heavily depends on the composition of matrix A and the vector \textbf{b}. We show that in specific cases where the matrix \( A \) is a Latin square and the vector \( \mathbf{b} \) satisfies certain constraints, the system has a unique solution in both the max-plus (\(\omega = 1\)) and min-plus (\(\omega = \frac{1}{n}\)) approaches. Moreover, column permutations of A do not affect the existence of solutions. However, row and element permutations alter the system structure, meaning solutions are not always guaranteed.