6CCS3VER 2019-20 Project – 25% of your mark Deadline 13/12/2019 • Please make sure you read the instructions fully before you start implementing the project. • The project is done on the Xchek tool, available in all UG labs. • The final product of the project is the report accompanied by appropriate source code files for the models and the sets of properties. The source code files should be written in GCLang and compile in Xchek. Executing the properties should have the result described in your report. • In the project, you will implement a counter (modulo 8 and then modulo 16) as a binary model for Xchek and a set of properties. The stages of the project are as follows: 1. Build a model for the counter modulo 8 with binary variables in GCLang. Keep in mind that you will have to extend your model to a counter modulo 16 with minimum changes to the code. 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. 3. Show that one of your properties passes vacuously in the system; explain the reason for the vacuous pass and fix the model or the property. 4. Introduce a bug in your model that is not caught by any of the properties. 5. Explain why this happened and write an additional property that exposes this bug. Demonstrate a counterexample. 6. Does your initial model satisfy this additional property? If no, explain why not and fix the model. 7. Extend your model to a counter modulo 16. Your initial design should have been general enough to allow this with a small number of changes. Explain the changes. 8. Out of the list of the properties you wrote, indicate which ones pass in counter modulo 16 and which fail. If none fail, introduce a new property that distinguishes between the counter modulo 8 and counter modulo 16 (that is, passes in one of them and fails in the other). • In your report, include drawings of your models as Kripke structures. • Projects that do not compile or do not run on Xchek will receive 0. Properties that are grammatically incorrect and hence cannot be understood by Xchek will lead to reduction in the mark (depending on the number of grammatically incorrect properties). Reports without Kripke structures will receive reduced marks for question 1. • Marking scheme: 30% for the model (question 1), 10% for each of the questions 2-8.
