联系方式

  • QQ:99515681
  • 邮箱:99515681@qq.com
  • 工作时间:8:00-21:00
  • 微信:codinghelp

您当前位置:首页 >> Python编程Python编程

日期:2020-12-21 11:19

6CCS3VER 2020-21

Project – 30% of your mark

Deadline 18/12/2020

? 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 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 system that simulates a counter (modulo 8 and

then modulo 16) interacting with the environment 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 that counts the number of times a variable

has the value 1 modulo 8 with binary variables in GCLang. In other words,

one of your variables should be a free variable, and the transitions of the

counter should depend on the value of this free variable. 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.

Clarification: answer “none of my properties pass vacuously” will not be

accepted – please have one of the properties passing vacuously.

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 (that counts the number of

times the free variable has the value 1). 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 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 (subquestions 1,3,4,5,6 for the model of counter modulo 8,

subquestion 7 for the model of counter modulo 16; for subquestion 8 both models

should compile and run). 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 the matching subquestions 1.

? Marking scheme: 30% for the model (question 1), 10% for each of the questions

2-8.


版权所有:编程辅导网 2021 All Rights Reserved 联系方式:QQ:99515681 微信:codinghelp 电子信箱:99515681@qq.com
免责声明:本站部分内容从网络整理而来,只供参考!如有版权问题可联系本站删除。 站长地图

python代写
微信客服:codinghelp