Please use this identifier to cite or link to this item:
|Title:||Automatic interface generation for enumerative model checking|
Pace, Gordon J.
|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 . 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:
|Proceedings of CSAW'06 - A19.pdf||144.81 kB||Adobe PDF||View/Open|
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.