A Healthcare Case Study: Fillwell

We describe a case study on a liquid handling workstation, Fillwell, that has been conducted within the EU-project MATISSE as a co-operation between academia and industry. Since the workstation is a safety-critical system that need to operate with very high precision, it need to be safe and very reliable. These aspects are achieved by developing the system using formal methods where the safety analysis goes hand in hand with the formal development. We use the B Action Systems formalism for the development, where we can benefit from the properties of action systems for designing distributed systems and on the tool support via the B Method. The development is performed in a stepwise manner adding new features to the system in each step. We use UML as a graphical interface to the formal methods to achieve a better acceptance of the methodology by the industrial partner. UML diagrams are created for all the refinement steps. Hence, UML provides us with a documentation of the whole development process. The stepwise development and the graphical interface of our method has shown to be a suitable approach for applying formal methods on this industrial sized case study.