Introduction
SWEN90010: HIGH INTEGRITY SYSTEMS ENGINEERING DEPARTMENT OF COMPUTING AND INFORMATION SYSTEMS THE UNIVERSITY OF MELBOURNE
Workshop Alloy – Traces Modelling
This workshop continues even further with formal modelling in Alloy and using the Alloy Analyzer. The aim is to get experience with checking invariants of state machine models, and with trace-based modelling (i.e. reasoning about traces of transitions in such models).
Copyright By PowCoder代写 加微信 powcoder
We will be continuing with the cacheMemory.als model from the previous workshop.
Your tasks
1. Download and open the cacheMemory.als specification from the LMS. This specification has been slightly modified since the last workshop so make sure you download the version for this workshop.
2. In this workshop we will investigate checking whether the cache system satisfies the following invariant: No memory address is present in both the cache and the main memory.
Write a predicate inv that encodes this property.
3. We can use Alloy to help us reason about whether this invariant will always hold, by getting it to check two
(a) The initial state satisfies the invariant. (b) Each operation preserves the invariant.
The cache system has the operations: write, read, load, and flush.
Write assertions to specify the two conditions above. Note that for the second condition we usually encode it as a collection of assertions: one for each of the operations.
Use Alloy to check these assertions. Which operations preserve the invariant and which don¡¯t? Examine the counter-examples that Alloy finds to understand why certain operations don¡¯t preserve the invariant.
What are the smallest bounds for which the counter-examples show up?
4. Given that some of the operations don¡¯t preserve the invariant, we can expect that from the initial state the system could reach a state in which the invariant doesn¡¯t hold. However, the checks above don¡¯t tell us what this sequence of operations might be. We will use Alloy to generate such a sequence of operations by modelling traces of transitions.
Write a fact first init that states that the first state in the trace is an initial state, i.e. satisfies the init predicate.
Then write a fact trans that states that it is always the case that either one of the cache system operations occurs or the state remains unchanged. Hint: You should write a predicate that specifies what it means for the cache system state to remain unchanged during a transition and use that predicate in your fact.
5. Write an assertion that says that it is always the case that the invariant holds. Use Alloy to check this assertion and to generate a trace in which the system starts in the initial state and then performs a sequence of operations to reach a state in which the invariant is violated.
6. After you add the first init fact you might find that some of your earlier checks that produced counter- examples no longer do so. Specifically the checks that each operation preserves the invariant.
There are two ways to write these checks, in gneral, for a state type State (which in this workshop is the CacheMemory type) and an operation predicate op:
all s:State | inv[s] and op[s] => after inv[s]
always all s:State | inv[s] and op[s] => after inv[s]
You should take one of the checks that produced a counter-example earlier and write it in each of the forms above. Work out which form produces the counter-example and which does not.
Think about why the first init fact prevents one of them from generating a counter-example but not the other. What does this tell you about the meaning of these two ways of writing invariant preservation assertions, in trace-based Alloy models? (i.e. in models that model traces of operations, not just individual transitions).
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com