基于xyz／e的ca认证系统描述与求精

时序逻辑语言xyz／e在统一的逻辑框架下既能表示静态语义又能表示动态语义，可以实现从抽象描述到可执行程序的平滑过渡。本文建立了ca认证系统组件求精模型，对ca和ra组件用xyz／e进行了描述和求精。