汽车黑匣子就是汽车行驶记录仪，它是用来记录汽车在行驶中的状态。随着黑匣子在飞机上的成功运用，越来越多的国家也在汽车上运用这种技术。早在1990年以前欧共体就通过了在汽车上安装黑匣子的立法，要求欧共体的15个成员国在10年内给使用中的900万辆商用车中安装这个装置。美国、台湾、香港及马来西亚等国家和地区也相继广泛使用汽车黑匣子[1]。从使用的效果来看，汽车黑匣......

模型校验是最成功的需求验证工具。模型校验的基本原理如图1所示。模型校验工具的输入是系统需求或设计(称为模型)以及最终系统期望实现的特性(称为“规范”)。如果给定的模型满足给定的规范，那么工具将输出yes，否则将生成反例。反例详细描述了模型无法满足规范的原因，通过研究反例，可以精确地定位模型的缺陷，如此反复。该方法的原理是通过确保模型满足足够多的系统特性以增强......