Institutional Repository
| 实时分布式时序语言XYZ/R | |
| 郭端阳 | |
| 1990 | |
| Degree Grantor | 中国科学院软件研究所 |
| Degree Level | 博士 |
| Place of Degree Grantor | 中国科学院软件研究所 |
| English Abstract | 实时分布式系统的广泛应用以及它对安全性的苛刻要求，使得应用形式化设计方法成为必要。本文设计了一种实时分布式时序逻辑语言XYZ/R，作为时序逻辑语言XYZ/E的扩充，XYZ/R在原有框架下扩充了时间“量”的概念，用来处理实时行为，它既是一种规范描述逻辑语言，又是一种实时程序设计语言，因而是一种ESPRIT计划中所要求的混合形式化方法。扩充的极大并发性模型被用来描述并发嵌套以及通讯传递时间等概念，在这个模型基础上，给出了XYZ/R的组合式语义。本文还给出了XYZ/R的一个证明系统，证明了在语义意义下的可靠性。XYZ/R的组合性支持实时系统层次化自顶向下逐步设计与验证。最后，文章针对一个实时系统的示例，给出了应用XYZ/R进行自高层描述、逐步分解与验证以及实现的全过程的设计。 |
| Abstract | 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. |
| Pages | 33 |
| Language | 中文 |
| Content Type | 学位论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/6016 |
| Collection | 中科院软件所_中科院软件所 |
| Recommended Citation GB/T 7714 | 郭端阳. 实时分布式时序语言XYZ/R[D]. 中国科学院软件研究所. 中国科学院软件研究所,1990. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment