中文摘要：

在本项目中，1、通过引进新的时序算子对原来的时序逻辑语言XYZ/E进行了扩充，使得XYZ系统既支持两栖系统和实时系统的描述、验证以及逐步求精过程；同时又保证了原来的逻辑基础不发生根本改变，从而使得XYZ系统原有的一些工具和方法能继续应用于两栖和实时系统的形式化分析。2、用扩充了实时性和两栖性的时序逻辑语言XYZ/E表示了Abrial蒸汽锅炉控制问题的形式规范以及从形式规范到实现的逐步求精过程。3、实现了蒸汽锅炉问题的一个可视化界面，并对在XYZ系统下两栖系统的形式化验证方法进行了一些研究。本项目已按计划完成，达到了预定的目标。