# Coloured Petri Nets-Based Modeling and Validation of Insulin Infusion Pump Systems
## 4 Model-Based Approach
### First System Refinement
#### 4.2.2 Software Module  
We divide the software module into three parts related to the steps of intermediate modular decomposition: battery verification, pump configuration, and insulin infusion. The battery verification starts from the Battery Situation transition (Figure 7), sending a message to the hardware to obtain the current status of the battery. The software receives a valued message from the hardware (ValueCharge(b1)) carrying the current status and verifies if the battery is charged enough to continue working. Otherwise, in addition to releasing the battery verification event, the software releases the battery recharge sending a Recherge(1) message to the Battery module. If there is more than one battery, the software sends the notification and continues working normally. The initial marking of the fusion place called Ok_B specifies the system contains only one battery. If there is more than one battery, the software can send a recharge message to a discharged battery and keep using the charged ones. When all batteries are discharged, the pump stops running, activated again after charging at least one battery. The initial marking of the fusion place Ok_B specifies that the system contains only one available battery. To start using the system, the user should configure the pump by defining the profile that guides operations: standard or personalized. The values' configuration for insulin dosages changes depending on the profile under consideration. The software sends a message to the hardware requiring the current cartridge's capacity to start configuring the pump. The capacity and the insulin dosages for basal, bolus, and bolus corrective are sent to a place named DC. The constants BASAL, BOLUS and CROLUS are used to configure predefined dosage values. Thus, the system can only administrate insulin dosages when these rules are satisfied. Figure 6: The hardware module of insulin infusion pump systems with two batteries. For the personalized mode, it is necessary to define values for different dosages daily. A text file, identified using a FILE constant, loads the configuration dosages to define the infusion mode values as list data structures, depending on the medical prescription for a specific clinical case. The remainder of the configuration follows the same approach as the standard mode. At the end of the configuration, two lists represent the basal and bolus dosages (called listBa and listDC), being the inputs for the insulin infusion step. Besides describing the insulin infusion pump system's configuration step, the reference model contains standard and personalized infusion modes specifications. Finally, the model includes a submodule for the standard infusion. The first step comprises recording the configuration data, notifying that the pump is executing and loading the cartridge. Afterward, it is possible to select a specific mode by firing one of the transitions called Adm Basal, Adm CBolus, and Adm Bolus. The pump's user can choose one or more types of insulin during the system execution. If the sum of all dosages does not exceed a safety limit, the system applies a unique dosage composed of all insulin; otherwise, the system applies the maximum allowed quantity of insulin dosage. Once the system is according to all preconditions, it applies the insulin and updates the cartridge's capacity. When there is no more insulin, the system transits to a state that indicates the need to fulfill the cartridge. The system also reaches this state when the cartridge's capacity is below the current insulin dosage being applied. For both situations, the pump transits from the partial state of executing. When the user recharges the pump, the system returns to the partial state of executing.