  Rigorous development processes aim to be effective in developing critical
systems, especially if failures can have catastrophic consequences for humans
and the environment. Such processes generally rely on formal methods, which can
guarantee, thanks to their mathematical foundation, model preciseness, and
properties assurance. However, they are rarely adopted in practice. In this
paper, we report our experience in using the Abstract State Machine formal
method and the ASMETA framework in developing a prototype of the control
software of the MVM (Mechanical Ventilator Milano), a mechanical lung
ventilator that has been designed, successfully certified, and deployed during
the COVID-19 pandemic. Due to time constraints and lack of skills, no formal
method was applied for the MVM project. However, we here want to assess the
feasibility of developing (part of) the ventilator by using a formal
method-based approach. Our development process starts from a high-level formal
specification of the system to describe the MVM main operation modes. Then,
through a sequence of refined models, all the other requirements are captured,
up to a level in which a C++ implementation of a prototype of the MVM
controller is automatically generated from the model, and tested. Along the
process, at each refinement level, different model validation and verification
activities are performed, and each refined model is proved to be a correct
refinement of the previous level. By means of the MVM case study, we evaluate
the effectiveness and usability of our formal approach.
