In my thesis I looked into the area of hemodialysis machines. I have examined a chronic and acute machine supervisor software architecture in more detail. Both softwares were made in C programming language, but while the chronic machine software has been prepared with traditional software development techniques, the acute machine software has been developed with an objective-oriented approach.
Then I examined some suitable methods for formal software development. I chose Event B and B method. With these methods, taking into account the OOP approach, I have created several models. I created two Event B models, the first is for representing the requirement modeling, the second is for examining the opportunities for reuse and team work. The B model is used for presenting the requirement modelling possibilities.
According to these models I could represent the advantages and disadvantages of these modelling methods. Both methods can be used for requirement modelling and C code generation, although it is difficult to integrate these generated codes into an existing software project especially the Event B model.
Based on these experiments, I can conclude, that both of these methods can be used for software development, but only in special cases, and the adoption of these methods is really time-consuming and expensive.