形式化建模在CTCS-3列控系统中的应用(4)
Multos信用卡认证系统，由国际信用卡联盟（万事达）开发，该系统负责处理信用卡用户存取交易时的身份验证, 做法是把系统中安全相关的关键部分和其它部分隔离开,在系统一级使用Z和CSP进行形式规范。
Eurocopter公司民用直升机自动导航系统，该公司组要是在嵌入式软件系统方面是有形式化方法，在编码阶段广泛使用SCADE的C代码自动生成工具，大量节省了写代码和测试代码的时间[8]。
2.1.2 形式化方法的特点介绍
当在系统设计和过程中采用形式化方法，可以方便地描述其可操纵性，并且可以分析和推算这些规范的正确性，从而证明我们系统的安全性。
经过分析和研究发现形式化方法具有以下的特点的：
表2.1形式化方法的特点
主要方面 特点详解
变量类型精确 变量类型描述精确，类型的定义有严格语义的数学概念(如自然，精确地描述输入、输出关系的行为。
形式化论证 形式化验证通过对需求分析中所描述的系统行为提供逻辑的精确论证。
目标系统特性明确 确切地指明了目标系统各方面的特性，实现了系统的重复分析、一致性分析以及较少依赖特定分析者技术和毅力的分析。
开发灵活 在开发早期就能够发现系统中可能存在的错误，可以避免因为已经建立完成后才发现缺陷的麻烦。
系统设计工具功能强大 形式化描述和验证是基于计算机的工具所支持，这使得一致性检查和证明等实现了自动化，提高了系统的可靠性，减少了在分析方面的费用。同时，这些工具容许证明能够被重复执行而大大增强了分析的重复性。
2.2 时间自动机
2.2.1 时间自动机的历史和基本功能的介绍
UPPAAL是由瑞典Uppsala 大学的信息技术学院和丹麦Aalborg大学的计算科学学院联合开发的。当前官方的发布版本为 UPPAAL4.0.13（2010年）。该工具选用一组带有整型变量的时间自动机对有实时性要求的系统行为进行模拟、对它的性质进行验证。所采用的验证机制可以避免状态空间爆炸问题，已得到广泛应用[9]。
时间自动机通过增加几个或者多个时钟约束，设置不同的转换条件，只有系统在规定的条件下才能进行下一步的操作，如果系统不满足不变式的约束，那么他将会只停留在当前的位置。建立时间系统标准模型都是采用时间自动机的，这是依据其具有很强表达时间能力。时间自动机有有限多个控制位置、有限多个实型值时钟。两个控制位置之间可能存在转换，仅当与之相联系的时钟约束都满足转换才有可能发生。转换发生改变了自动机的停留的控制位置，并重置了相应的时钟[10] 。
上一篇：MATLAB红外图像去噪算法研究
下一篇：动车组转向架轴承故障诊断+源程序