1. Alloy Modelling Overview

签名（Signatures）：在Alloy中声明集合和关系。
事实（Facts）：作用在签名上的全局约束，排除模型中的无意义部分。
谓词（Predicates）：在模型中定义变量之间的关系，用于指定操作、状态转换。
函数（Functions）：表达式的简写。

2. 有限状态机（Finite State Machines）

从初始状态s0开始
状态是不同类型变量的集合。有一系列操作，每个操作都改变状态。每个操作实现不同的状态转换。

3. 在Alloy中建模有限状态机（Modelling FSMs in Alloy）

状态是（类型化的）变量的集合： sig State {…}
可能使用约束：fact blah { always all s : State | … }
初始状态：pred Init[s : State] { … }
操作：pred Op1[s : State] { … } pred Opn[s : State] { … }
谓词可能使用函数作为简写
示例：

4. 在Alloy中检查规格（CHECKING SPECIFICATIONS IN ALLOY）

校验一个规格
- 我们如何知道我们的规格正确地捕获了我们的意图？
- Animation 动画（运行规格以查看它捕获的行为）
- Check Assertions 检查断言（看看哪些属性可能从规格中推导出来）

4.1 Alloy的run命令

- 查找满足在指定边界内的谓词的实例
- 从最小的合理边界开始，如果无法满足，则增加它

4.2 Alloy的assert语句

- 声明应从规格中推导出的属性。

4.3 Alloy的check命令

- 在固定的边界内搜索违反属性的反例。
- 使用“expect”来注解哪些检查应通过，哪些应失败
- 从最小的合理边界开始，如果找不到反例，则增加它

5. deletelsUndo示例

无效的反例（Invalid Counterexamples）

断言作为测试

Alloy进行有界的断言检查 Alloy does bounded assertion checking
像在边界内测试一个断言 Like testing an assertion for all systems up to the bound
不能证明断言在任意大小的系统中总是成立 Doesn’t prove the assertion will hold for systems of arbitrary size in general
尽管在特定的系统和断言中可能是这样。Although it might for specific systems and assertions.
总的来说，如果不是证据，它给出了非常高的信心。In general, it gives very high confidence if not a proof.

断言的信心（Assertion Confidence）

如果Alloy说所有的断言都成立，我的规格是对的吗？
- 否
- 只在有限的边界内检查。Checks only within finite bounds.
- 规格可能不完整。Spec could be incomplete.
- 规格可能说了错误的事。Spec could say the wrong thing.

高完整性系统工程（四）： Checking Formal Specifications相关推荐

高完整性系统工程（三）： Logic Intro Formal Specification
目录 1. Propositions 命题 2.1 Propositional Connectives 命题连接词 2.2 Variables 变量 2.3 Sets 2.3.1 Set Operat ...
高完整性系统工程（一）：Intro Safety
制作满足用途的大型软件的方法 Criteria(标准) Security 安全性 Correctness 正确性 Performance 绩效 Reliability 可靠性 Usability 可用 ...
高完整性系统工程（九）：Invariants
目录 1. INVARIANTS 1.1 例子 1.2 正式的证明 1. INVARIANTS 一个不变式需要满足以下三个属性: 当循环开始时,不变式是正确的在每一次循环迭代之后,不变式仍然是正确的 ...
高完整性系统工程（一）： Safety Engineering, HAZOP Fault Tree Analysis
目录 1. 因果性不等同于相关性 2. HAZOP 2.1 学习HAZOP 2.2 HAZOP概览 2.3 Assessing Hazard Risks 评估 2.4 示例场景 2.5 HAZOP G ...
高完整性系统工程（十一）：Fault Tolerant Design
目录 1. INTRODUCTION TO FAULT TOLERANCE 1.2 Definitions 1.3 Two Kinds of Faults 1.4 Hardware vs Softwa ...
高完整性系统 (2)：Requirement 与 Design 阶段的风险控制——Hazards, HAZOP, Fault Tree
文章目录安全性工程流程 Hazards 反事实推理(CounterFactual Reasoning) 案例1 案例2 案例3 HAZOP: HAZARDS AND OPERABILITY STUD ...
深度学习（15）TensorFlow高阶操作四: 填充与复制
深度学习(15)TensorFlow高阶操作四: 填充与复制 1. Pad 2. 常用于Image Padding 3. tile 4. tile VS broadcast_to Outline pa ...
高仙机器人四十万能级生产基地项目开工仪式在四川资阳举行
9月29日,高仙机器人四十万能级生产基地项目开工仪式在四川省资阳市临空经济区(清泉)智能制造产业园举行.资阳市委书记元方,高仙机器人董事长.首席执行官程昊天,四川省清洁服务行业协会会长刘英勇,电子科技 ...
【高数】高数第四章节——不定积分换元积分分部积分
高数第四章节--不定积分&换元积分&分部积分 0.博主高数相关章节目录 1.数列 1.不定积分的概念与性质 1.1 原函数 1.2 不定积分 1.3 不定积分的性质 1.3.1 性质 ...

高完整性系统工程（四）： Checking Formal Specifications

1. Alloy Modelling Overview

2. 有限状态机（Finite State Machines）

3. 在Alloy中建模有限状态机（Modelling FSMs in Alloy）

4. 在Alloy中检查规格（CHECKING SPECIFICATIONS IN ALLOY）

4.1 Alloy的run命令

4.2 Alloy的assert语句

4.3 Alloy的check命令

5. deletelsUndo示例

高完整性系统工程（四）： Checking Formal Specifications相关推荐

最新文章

热门文章