Please use this identifier to cite or link to this item:
Title: Automatic interface generation for enumerative model checking
Authors: Spina, Sandro
Pace, Gordon J.
Keywords: Compositionality (Linguistics)
Computer interfaces
State-space methods
Issue Date: 2006
Publisher: University of Malta. Faculty of ICT
Citation: Pace, G. J., & Spina, S. (2006). Automatic interface generation for enumerative model checking. 4th Computer Science Annual Workshop (CSAW’06), Bighi. 1-7.
Abstract: Explicit state model checking techniques suffer from the state explosion problem [7]. Interfaces [6, 2] can provide a partial solution to this problem by means of compositional state space reduction and can thus be applied when verifying interestingly large examples. Interface generation has till now been largely a manual process, were experts in the system or protocol to be verified describe the interface. This can lead to errors appearing in the verification process unless overheads to check the correctness of the interface are carried out. We address this issue by looking at automatic generation of interfaces, which by the very nature of their construction can be guaranteed to be correct. This report outlines preliminary experiments carried out on automatic techniques for interface generation together with their proofs of correctness.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
Proceedings of CSAW'06 - A19.pdf144.81 kBAdobe PDFView/Open

Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.