MOBS_OM_MK_GF_HEALTHINF_2015

Ben Salem, M. O.; Mosbahi, O.; Khalgui, M.; Frey, G.: ZiZo: Modeling, Simulation and Verification of Reconfigurable Real-Time Control Tasks Sharing Adaptive Resources - Application to the Medical Project BROS. 8th Int. Conference on Health Informatics (HEALTHINF 2015), Lisbon, Portugal, pp. 20-31, Jan. 2015.

 

Abstract

This research paper deals with the modeling, simulation and model checking of reconfigurable discrete-event control systems to be distributed on networked devices. A system is composed of software tasks with shared resources to control physical processes. A reconfiguration scenario is assumed to be a run-time automatic operation that modifies the system’s structure by adding or removing tasks or resources according to user requirements in order to adapt the whole architecture to its environment. Nevertheless, a reconfiguration can bring the system to a blocking problem that is sometimes unsafe, or violates real-time properties. We define new Petri Nets-based modeling solutions for both tasks and resources to meet these constraints. These solutions are applied to a real case study named Browser-based Reconfigurable Orthopedic Surgery (abbrev. BROS) to illustrate the paper’s contribution. A new Petri Nets-based editor and random-simulator named ZiZo is developed to model and simulate the BROS reconfigurable architecture. It is based also on the model checker SESA to apply an exhaustive CTL-based formal verification of this architecture to ensure safe reconfiguration scenarios of tasks and resources.

Keywords: Distributed Control System, Reconfiguration, Shared Resource, Simulation, Verification, Model Checking, Computer-assisted Surgery.