A Compositional Proof Theory for Real-Time Distributed Message Passing
A Compositional Proof Theory for Real-Time Distributed Message Passing
复制标题
实时分布式消息传递的组合证明理论
DOI：
10.1007/3-540-17945-3_18
复制
发表时间：
1987
期刊：
影响因子：
--
通讯作者：
J. Hooman
中科院分区：
文献类型：
--
作者：
J. Hooman
本文给出了一种基于同步消息传递的分布式计算的类OCCAM实时程序设计语言的组合证明系统。该证明系统基于独立于这些进程的程序文本的进程规范。这些规范陈述了（1）过程关于其环境行为的假设，以及（2）该过程对该环境的承诺，前提是满足这些假设。证明系统是健全的w.r.t的指称语义，其中包括关于环境的动作的假设，从而密切近似的假设/承诺推理的风格，证明系统的基础上。并发性被建模为“最大并行性”;也就是说，如果一个进程可以继续，它将立即继续。进程只在没有本地操作可能并且没有伙伴可用于通信时等待。这个极大性属性被强加在断言的解释域上，把它假定为单独的公理。一个系统的时间行为是从一个全局外部观察者的角度来表达的，所以有一个全局的时间概念。时间不一定是离散的。
A compositional proof system is given for an OCCAM-like real-time programming language for distributed computing with communication via synchronous message passing. This proof system is based on specifications of processes which are independent of the program text of these processes. These specifications state (1) the assumptions of a process about the behaviour of its environment, and (2) the commitments of that process towards that environment provided these assumptions are met. The proof system is sound w.r.t a denotational semantics which incorporates assumptions regarding actions of the environment, thereby closely approximating the assumption/commitment style of reasoning on which the proof system is based. Concurrency is modelled as "maximal parallelism"; that is, if a process can proceed it will do so immediately. A process only waits when no local action is possible and no partner is available for communication. This maximality property is imposed on the domain of interpretation of assertions by postulating it as separate axiom. The timing behaviour of a system is expressed from the viewpoint of a global external observer, so there is a global notion of time. Time is not necessarily discrete.