Please use this identifier to cite or link to this item: http://repositorio.inesctec.pt/handle/123456789/4182
Title: Bounded Model Checking of Temporal Formulas with Alloy
Authors: Alcino Cunha
Issue Date: 2014
Abstract: Alloy is a formal modeling language based on first-order relational logic, with no native support for specifying reactive systems. We propose an extension of Alloy to allow the specification of temporal formulas using LTL, and show how they can be verified by bounded model checking with the Alloy Analyzer. © 2014 Springer-Verlag.
URI: http://repositorio.inesctec.pt/handle/123456789/4182
http://dx.doi.org/10.1007/978-3-662-43652-3_29
metadata.dc.type: conferenceObject
Publication
Appears in Collections:HASLab - Articles in International Conferences

Files in This Item:
File Description SizeFormat 
P-009-NJ5.pdf198.27 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.