嵌入式系统的自动验证技术

本项目“嵌入式系统的自动验证技术”对嵌入式系统的计算模型、规范语言、验证方法和工具进行系统深入的研究。建立了statetecharts的一种时态逻辑语义。提出了一种新的嵌入式系统规范语言Accumulation Calculus,并建立了Accumulation Calculus的一个相对完备的公理系统。提出了一种将定理征明技术和模型检查技术的优点，并且部分解决了仅用模型检查技术不能解决的问题，在对嵌入式系统基准案例Gas Burner的验证中得到了最优的结果。