实时电路的形式化描述和验证

该项目研究建立了平均值演算的理论基础。给出了形式语义，证明系统、完全性定理和可判定理的证明。用平均值演算对实时电路做了充分的研究，得出了实时电路在连续时间模型上不可判定和在离散时间模型上可判定的结论。对实际计算机中央处理器进行了描述和验证。给出了目前工业界硬件设计语言Verilog HDL的形式语义。完成了数篇论文。