摘要
Z是一种确定相关数据特征的非常成功的形式化语言,却在构造动态行为方面的模型缺乏相应的功能;而TimedCSP是一种确定动态行为的功能强大的语言,但它没提供适当的结构来构造相关数据特征。文中通过形式化语言Z和过程代数TimedCSP合成一种新的形式化方法RT-Z,使得RT-Z在软件系统开发过程的需求定义和设计阶段能书写软件系统一致、简单的规格说明。
Z is a successful formal language of specifying data - related characteristics, but it is not designed to model aspects of the dynamic behaviour. Timed CSP is a powerful language for the dynamic behaviour, hut it doesn＇ t provide adequate constructs to model data - related characteristics, This paper combines the formal specification languages Z and timed CSP, called RT - Z. RT - Z is intended to be used in the requirements definition and de.sign phases of the system and software development process, RT - Z can achieve a single, uniform specification, A case is forwarded to illustrate the usage of RT - Z in writing software specification.
出处
《微机发展》
2005年第8期34-36,40,共4页
Microcomputer Development
基金
国家自然科学基金资助项目(6047407260174050)
广东省自然科学基金资助项目(04009465010059)
广东省高校自然科学研究项目(Z03024)
