An Executable Semantics of Object-oriented Models for Simulation and Theorem Proving

This paper presents an executable semantics of OO models. We made it possible to conduct both simulation and theorem proving on the semantics by implementing its underlying heap memory structure within the expressive intersection of the functional language ML and the theorem prover HOL. This paper also presents a verification system ObjectLogic which supports simulation and theorem proving of OO models based on the executable semantics. As an application example, we show a verification of a UML model of a practical firewall system.

• Type: Conference
• Year: 2008
• Where: VVEIS
• Authors: Kenro Yatake, Takuya Katayama
• Keywords: Executable Semantics, Information Technology, OO Models, Theorem Proving, VVEIS 2008