# COMPSYS705 代写 Exam 代考
## 1. 考试信息
– **考试日期**：2023年10月17日
– **考试科目**：COMPSYS 705 Formal Methods for Safety Critical Software Test
– **总分**：100分
– **权重**：50%
– **答题要求**
– 回答所有问题，Part I占70分，Part II占30分。
– 问题1 – 4属于Part I，其余属于Part II。
– 展示问题5和6的所有代码。
– 在提供的框内作答，答案应清晰可读。
## 2. 题目及答题框
### Q1（20分）
1. **关于进程代数CCS的问题（20 Marks）**
– **(a) 进程相似性判断（5 Marks）**
– 考虑图1中的两个进程$P, Q$，判断它们是否双相似、弱双相似、相似或无关系，并通过数学方法证明。
– **(b) 绘制LTS（10 Marks）**
– 考虑由方程1和方程2分别定义的两个进程$P$和$Q$，绘制它们各自的标签转换系统（LTS）以及$P \| Q$的LTS（只绘制到第二层后继）。
– **(c) 模拟和双模拟的比较（5 Marks）**
– 比较模拟和双模拟哪个更强，并通过合适的例子证明。
2. **Q1答题框**
### Q2（20分）
1. **时态逻辑与模型检查（20 Marks）**
– **(a) 模型检查步骤（10 Marks）**
– 展示在图2所示模型上对公式$A F(\neg P 1 \Lambda \neg P 2) \vee P 3$进行模型检查的所有步骤，并判断模型是否满足该属性。
– **(b) 识别有效CTL公式（10 Marks）**
– 从给定的公式中识别出有效的CTL公式，并给出合理的理由，将识别出的有效公式转换为仅使用适当集合的等价形式（只能包含时态运算符$E X, E G, E U$）。
2. **Q2答题框**
### Q3（20分）
1. **实时系统与自动机（20 Marks）**
– **(a) 自动机相关问题（10 Marks）**
– 设$\sum ={a, b, c, d}$，$A1$和$A2$是图3所示的两个自动机，要求绘制乘积自动机，判断$bbabab^{*}$是否被$A1$接受，$b^{*}d^{*}a^{*}b^{*}$是否被$A2$接受，$bbbb^{*}a^{*}d^{*}c^{*}$是否被$A1\cap A2$接受，$aabc^{*}d^{*}b \in \sum ^{*}$是否成立，并给出理由。
– **(b) 时钟约束有效性判断（5 Marks）**
– 在定时自动机中，判断给定的时钟约束哪些是有效的，并说明原因（假设$x, y, z$是时钟）。
– **(c) 运行时验证和运行时强制的区别（5 Marks）**
– 区分运行时验证和运行时强制，并说明哪一个更适合用于保护心脏起搏器以及原因。
2. **Q3答题框**
### Q4（10分）
1. **简答题（10 Marks）**
– **(a) 运行时验证监控器工作原理（5 Marks）**
– 使用合适的图表解释如何在不直接访问心脏起搏器的情况下，利用运行时验证来保护心脏起搏器的监控器的工作原理。
– **(b) 示例属性（5 Marks）**
– 提供一个作为定时自动机的示例属性，该属性可被运行时验证监控器用于确定心脏起搏器是否被使用ECG传感器攻击。
2. **Q4答题框**
### Q5（15分）
1. **函数等价性证明（15 marks）**
– 证明`swap1`和`swap2`函数对于所有相同的`int`类型输入`a`和`b`返回相同的交换值，使用Z3 Python API将等价性（验证）问题编码为SMT约束，并展示Python代码。
2. **Q5答题框**
### Q6（15分）
1. **有限状态机相关问题（15 marks）**
– **(1) 绘制异步乘积FSM（5 marks）**
– 图4给出了在单个CPU上执行的两个FSM，绘制它们的异步乘积作为单个FSM。
– **(2) 使用Python Z3 API建模路径（5 marks）**
– 使用Python Z3 API对异步乘积FSM的所有路径进行建模。
– **(3) 检查LTL安全属性（5 marks）**
– 使用Python API向Z3提出LTL安全属性$\square(\neg((S1==1) \Lambda(S2==1)))$，以便在（2）中建模的路径上检查该属性，展示所有Python代码和图形。
2. **Q6答题框**