| 实时分布式时序语言XYZ/R |
| 郭端阳
|
| 1990
|
| 学位授予单位 | 中国科学院软件研究所
|
| 学位 | 博士
|
| 学位授予地点 | 中国科学院软件研究所
|
| 摘要 | 实时分布式系统的广泛应用以及它对安全性的苛刻要求，使得应用形式化设计方法成为必要。本文设计了一种实时分布式时序逻辑语言XYZ/R，作为时序逻辑语言XYZ/E的扩充，XYZ/R在原有框架下扩充了时间“量”的概念，用来处理实时行为，它既是一种规范描述逻辑语言，又是一种实时程序设计语言，因而是一种ESPRIT计划中所要求的混合形式化方法。扩充的极大并发性模型被用来描述并发嵌套以及通讯传递时间等概念，在这个模型基础上，给出了XYZ/R的组合式语义。本文还给出了XYZ/R的一个证明系统，证明了在语义意义下的可靠性。XYZ/R的组合性支持实时系统层次化自顶向下逐步设计与验证。最后，文章针对一个实时系统的示例，给出了应用XYZ/R进行自高层描述、逐步分解与验证以及实现的全过程的设计。 |
| 其他摘要 | A distributed real-time temporal logic XYZ/R is proposed. As an extension of XYZ/E, XYZ/R incorporates a quantitative notion of time within temporal logic and gives rise to a mixed formalism, characterized both as a specification logic and a real-time programming language. Real-time concurrency is modeled by an extension of the maximal parallelism model of Salwicki and Muldner, that no process waits unnecessarily, and the modeling of nested parallelism and transmission time for communication is included. We have given a proof system, which is sound with respect to its semantics. Compositionality in this formalism makes it possible to specify and verify distributed real-time system hierarchically. An example demonstrates that our approach can support the whole process of real-time system development, from requirement specification to implementation programming. |
| 页数 | 33
|
| 语种 | 中文
|
| 内容类型 | 学位论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/6016
|
| 专题 | 中科院软件所_中科院软件所
|
推荐引用方式
GB/T 7714 |
郭端阳. 实时分布式时序语言XYZ/R[D]. 中国科学院软件研究所. 中国科学院软件研究所,1990.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论