摘要:Makalah ini mendeskripsikan model formal dari sistem interaktif berdasarkan sebuah studi kasus pada sistem kesehatan bergerak. Model ini mendeskripsikan sebuah session interaktif melibatkan profesional medis yang menggunakan PDA untuk mengakses rekam medis pasien, dan terhubung pada server basis data dalam jaringan komunikasi nirkabel. Perilaku sistem dapat memunculkan masalah keselamatan bila dikaitkan dengan perilaku pemakai dalam pelayanan kesehatan. Akhirnya model sistem telah diverifikasi untuk menghindari masalah tersebut. Kata kunci: metode formal, sistem interaktif, sistem perawatan kesehatan bergerak