Bounded Model Checking of Temporal Formulas with Alloy
Software Engineering
2015-06-26 v3 Logic in Computer Science
Abstract
Alloy is formal modeling language based on first-order relational logic, with no specific support for specifying reactive systems. We propose the usage of temporal logic to specify such systems, and show how bounded model checking can be performed with the Alloy Analyzer.
Keywords
Cite
@article{arxiv.1207.2746,
title = {Bounded Model Checking of Temporal Formulas with Alloy},
author = {Alcino Cunha},
journal= {arXiv preprint arXiv:1207.2746},
year = {2015}
}
Comments
New version of the ABZ'14 paper that corrects a mistake in the encoding of the the U and R temporal operators