![[Maison.png]](../../images/Maison.png)
Back to Home| Abstract Automatic program verification belongs to the old quests of software engineering, and theoretic computer science. Though any definitive solution is fundamentally excluded due to theoretical considerations, some partial yet promising answers could be proposed so far, in particular Model-Checking. At the same time, Object Orientation has firmly established itself among practitioners as one of the most relevant programming paradigms. In this report, we address the connection between Model-Checking and Object-Orientation from a tool perspective. In a first part we try to give an overview of today's model checking state of the art with three representative tools among the most popular ones: Spin, SMV and Kronos. We introduce the spirits, the concepts, and the domain of application of each tool. In a second part, we move on to higher-level frameworks: vUML, UMLAUT and Bandera. Those tools take profit of the 'pure' model-checking engines presented before to allow the verification of Object Oriented Models. Among them, we identify 2 main approaches we refer respectively to as the preventive and the pragmatic one. We conclude with some considerations about the practical use of Model Checking methods. |
Back to Home