report | project代做 – 6CCS3VER 20 20 – 21 August resit

6CCS3VER 20 20 – 21 August resit

report | project代做 – 本题是一个利用report进行练习的题目

 project  30 % of your mark

• Please make sure you read the instructions fully before you start implementing the project.
• The project is done on the Xchek tool, available as a part of the KCL VM installation or as a standalone software http://www.cs.toronto.edu/~arie/xchek/ , and it works on Linux and Mac machines.
• The final product of the project is a single zip file containing the following files:

a. The  report with answers to the questions;

b. The source code files in GCLang for all models implemented as a part of the
project. The code should compile in Xchek.

c. The files with the CTL properties that you wrote to check your models in
Xchek. For each property, indicate the result of its execution in the report; this
will be checked as a part of the marking process.

• The stages of the project are as follows:
  1. Build a model M 1 for a counter modulo 4 with binary variables in GCLang. Use as few variables as possible. The initial state should correspond to 0. [10 marks]
  2. Write an initial set of CTL properties to check correctness of your model. Argue that the set represents the intuitive specification of what we can expect from the counter. For each property, indicate whether it is a safety property or a liveness property and explain why. [ 2 0 marks]
  3. Change your model so that it has two initial states: a state corresponding to 0 and a state corresponding to 1. The resulting model is M 2. [10 marks]
  4. Write a set of properties that demonstrates that M 2 indeed has two initial states. For each property, indicate whether it is a safety property or a liveness property and explain why. [ 2 0 marks]
  5. Do any of the properties you wrote in question 2 pass vacuously in M 1? Answer for each property: [ 2 0 marks]

a. If a property passes vacuously, show that there is a strengthened
version that also passes in M 1.

b. If a property passes but not vacuously, show an interesting witness
trace in M 1.

6. Extend M 1 to a counter modulo 6. Use as few variables as possible.

[10 marks]

7. Write a property that distinguishes between M 1 and the model you wrote in (6). That is, this property passes in one model and fails in the other.

[10 marks]

• In your report, include figures of your models as Kripke structures. If the model is too large, include a part of the figure and explain how the rest of the model looks like.
• Models that do not compile or do not run on Xchek will receive 0 for the relevant subquestions. Reports without Kripke structures will receive reduced marks for the matching subquestions.