基于XYZ／E的CA认证系统描述与求精

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