Abstract
Safety properties of a system may be specified by constraining the sequences of interactions of the system with its environment. This paper shows how to encode specifications in such a style using Alloy.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bolton, C.: Using Alloy to Automatically Verify the Soundness of the Simulation Rules for Reasoning about State-Based and Event-Based Models (2002), http://alloy.mit.edu/community/files/simulationDiscussion.ps
Jackson, D.: Software Abstractions: Logic, language and analysis. MIT Press, Cambridge (2006)
Hoare, C.A.R.: Communicating Sequential Processes. Series in Computer Science. Prentice Hall, Hemel Hempstead (1985)
Jacob, J.L.: Basic theorems about security. Journal of Computer Security 1, 385–411 (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jacob, J.L. (2010). Trace Specifications in Alloy. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds) Abstract State Machines, Alloy, B and Z. ABZ 2010. Lecture Notes in Computer Science, vol 5977. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11811-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-11811-1_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11810-4
Online ISBN: 978-3-642-11811-1
eBook Packages: Computer ScienceComputer Science (R0)