MedicationChecker: Development of a Formally Verified Android Application with EventB2SQL

摘要

In this work, we present a case study on the development of a formally verified Android application for checking medication interactions and contraindications. Combining formal methods and Model-View-Controller development methodologies, we created an Event-B model for the application, verified that no patient could be prescribed a medication that had an interaction or contraindication for them, generated code for the model and part of the user interface with the EventB2SQL tool, and then implemented the controller and the rest of the view by hand. We describe our experience in employing this methodology, enhancements to the EventB2SQL tool, and some notes on the performance and usability of the resulting application.