使用TLA对一个工业级安全协议的建模实现

论文摘要

目前越来越多的安全临界系统被应用到我们的日常生活中,以至于安全工程也越来越受到关注。在这种情况下,国际电子技术协会颁布了国际功能安全标准《IEC 61508》。这套功能安全标准使用安全集成度来描述系统安全性,并推荐了很多形式化方法作为安全检证的手段。形式化方法主要检验系统三个方面的属性是否满足,即:安全性,活性以及公平性。但是在实际操作中面临三个主要问题:其一,验证结论很难使用功能安全标准中安全集成度的度量标准进行描述;其二,形式化方法对系统所处的环境以及人机交互方面的处理比较薄弱,需要人为地针对性的加以处理;其三,绝大多数形式化方法是基于状态枚举原理的,无法回避状态爆炸问题。在论文探讨使用TLA对系统进行建模与分析之前,我们首先简单地介绍了一下TLA以及建模所需要的基础数学知识。随后我们在论文中提出了一种分治策略用于对系统规格说明进行抽象简化。其基本思想是将复杂的系统简单化,先提出一个最简单抽象的概念模型,然后逐层细化各个模块,将系统的功能和数据交互添加到这些模块中去。在这一过程中,我们由简入繁地反向分析哪些系统因素是安全相关的,哪些系统因素是可以在将来的模型中简化甚至省略掉的。这对简化系统复杂度起到了相当关键的作用。同时,我们可以逐渐分析出系统需要满足哪些安全性,活性以及公平性属性。为了更好地配合TLA建模,我们在分治策略中还提出了针对模块功能分析的模块状态机(Module State Machine)机制。分治简化结束后,其模块状态机可以很容易地转化为TLA模型。最后我们讨论了对系统的TLA模型进行验证的实验结果。这个结果表明,该系统的设计满足安全性属性要求。但是由于TLA以及其模型验证工具TLC的局限性,我们无法检验系统的活性和公平性属性,并且即使是已经简化的系统模型,也可能需要相当长的验证时间。对于这样的结果,我们详细分析了其原因,并指出了未来相关研究的方向。

论文目录

• 摘要
• Abstract
• Chapter 1 Introduction
• 1.1 Background
• 1.2 Properties Need to be Checked in Formal Verification
• 1.3 Problems
• 1.4 Proposal
• 1.5 Thesis Outline
• 1.6 Summary
• Chapter 2 Prerequisite Knowledge
• 2.1 Brief Explanation of TLA
• 2.2 Propositional Logic
• 2.3 Set Theory
• 2.4 Predicate Logic
• 2.5 Linear Temporal Logic
• 2.6 Summary
• Chapter 3 Divide and Conquer Paradigm for System Specification Refinement
• 3.1 Brief Explanation of Divide and Conquer Paradigm
• 3.2 Module State Machine for Representation of Specification
• 3.3 Detailed Steps of Using D&C Paradigm for Specification Refinement
• 3.4 Summary
• Chapter 4 System Specification Refinement
• 4.1 Concise System Specification
• 4.1.1 Telegram Structure
• 4.1.2 Communication Schema
• 4.1.3 Timing Restrictions
• 4.1.4 System States and Behaviors
• 4.1.5 Mutual Checking between MPU’s
• 4.2 System Division
• 4.2.1 System Overall Hierarchical Break-down Structure
• 4.2.2 First Level Division
• 4.2.3 Second Level Division
• 4.2.4 Third Level Division
• 4.3 System Conquest
• 4.3.1 Robot Refinement
• 4.3.2 Mutual Checking Refinement
• WHT Refinement'>4.3.3 SM_WHT Refinement
• HC Refinement'>4.3.4 SM_HC Refinement
• 4.3.5 Module Integration
• 4.4 Liveness and Fairness Properties Analysis
• 4.5 Summary
• Chapter 5 Implementation of Models in TLA
• 5.1 Implementation of Telegram Model
• 5.2 Implementation of MPU Model
• 5.3 Implementation of HC Model
• 5.3.1 Modeling Telegram Sending Logic
• 5.3.2 Modeling Telegram Receiving Logic
• 5.4 Implementation of WHT Model
• 5.5 Implementation of Mutual Checking Function
• 5.6 Implementation of Communication Channel Model
• 5.7 Implementation of Liveness and Fairness Property
• 5.8 Summary
• Chapter 6 Model Analysis
• 6.1 Verification Result of the System Model
• 6.2 Limitations of TLA and its Model Checker TLC
• 6.2.1 State Explosion Problem
• 6.2.2 Stuttering Steps
• 6.3 Summary
• Conclusion
• References
• Appendix
• Extended Abstract in Chinese
• Acknowledgement
• Resume