Paper Info
Title
An executable object-oriented semantics and its application to firewall verification
Abstract
This paper presents a formal executable semantics of object-oriented models. We made it possible to conduct both simulation and theorem proving on the semantics by implementing it within the expressive intersection of the functional programming language ML and the theorem prover HOL. In this paper, we present the definition and implementation of the semantics. We also present a prototype verification tool ObjectLogic which supports simulation and theorem proving on the semantics. As a case study, we show the verification of a practical firewall system.
Year
DOI
Venue
2011
10.1007/s10270-010-0160-1
Software and System Modeling
Keywords
Field
DocType
object-oriented · theorem proving · simulation · hol · ml,object-oriented model,prototype verification tool objectlogic,practical firewall system,executable object-oriented semantics,case study,expressive intersection,theorem prover,functional programming language,formal executable semantics,hol,theorem proving,object oriented,simulation
HOL,Operational semantics,Programming language,Computer science,Automated theorem proving,Denotational semantics,Action semantics,Theoretical computer science,Well-founded semantics,Semantics,Executable
Journal
Volume
Issue
ISSN
10
4
1619-1374
Citations 
PageRank 
References 
0
0.34
18
Authors
2
Name
Order
Citations
PageRank
Kenro Yatake1234.59
Takuya Katayama245598.24