Neuroboscope sisteminin model tabanlı sınaması

Abstract

NeuRoboScope projesinde, endoskopik hipofiz cerrahisinde kullanılan optik-kamera sisteminin, cerrahın kullandığı cerrahi aletleri takip ederek yönlendirilmesini amaçlayan emniyet kritik bir sistemin tasarlanması amaçlanmıştır. Bu bildiri, sistem gereksinimleri üzerinden tüm sistemin modellenmesini ve oluşturulan bu modelin sınanmasını ele almaktadır. Böylece, tasarım evresinden önce tasarımın dayanağı olan sistem gereksinimlerinin doğrulanması hedeflenmiştir. Sistem bir zamanlı otomat ağı olarak modellenmiş ve UPPAAL model sınama aracı kullanılarak, sistemin başta emniyet kritik olmak üzere diğer önemli özellikleri sınanmıştır.

In the NeuRoboScope project, it is aimed to design a safetycritical system that navigates the optical-camera system used in the endoscopic pituitary surgery by tracking the surgery tool that the surgeon uses. This study presents modeling the system upon the requirements and verification of this model, which allows to validate the system requirements before the design phase. Using UPPAAL model checking tool, the entire system is modeled as a network of timed automata and verified against the vital system properties, including particularly the safety critical ones.