一种基于时序逻辑语言的实时售票系统描述与精化方法  

A Method of the Description and Refinement of Real-time System of Selling Tickets Based on Temporal Logic

作　　者：金旗铭[1,2] 张广泉[1] 

机构地区：[1]苏州大学计算机科学与技术学院,江苏苏州215006 [2]苏州邮政局,江苏苏州215004

出　　处：《苏州大学学报（工科版）》2009年第4期16-21,共6页Journal of Soochow University Engineering Science Edition (Bimonthly)

基　　金：江苏省高校自然科学基金资助项目(编号08KJB520010)

摘　　要：时序逻辑语言XYZ/E在统一的形式框架下既能表示静态语义又能表示动态语义,可以实现从抽象描述到可执行程序的平滑过渡。分析了邮政汽车票售票系统的实时性,给出了该系统的组件模型,用XYZ/E描述了整个软件系统的体系结构,逐步精化了核心组件PCServer、PDClient、PSClient,实现了功能组件PSSComput1和PSSComput2到可执行程序XYZ/E的平滑过渡。The temporal logic language（TLL） XYZ/E can represent both dynamic semantics and static semantic under a unified framework and carry out the smooth transition from abstract specification to execuable program. This paper analyzes the Real-time property of the postal ticketing system, and presents the system＇s component model, using XYZ/E describes the entire system architecture and the progressive refinement of the core components PCServer, PDClient, PSClient. Realize the Refinement of the two functional components PSSComputl, PSSComput2 smooth transition to the executable program.

关 键 词：分布式实时系统 时序逻辑语言 XYZ/E 实时售票系统 描述 精化 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]