程序:物理对象上的操作表达式(英文)

把赋值语句看作物理对象上的操作时,程序就呈现为物理对象上的操作构成的表达式(简称O表达式)。给出了定义O表达式语法的BNF公式,并用公理规定O表达式的语义。主动式的O表达式以计算最终结果为目的,因而相关公理给出的是施行表达式中操作以后的变量与施行之前变量之间的准确依赖关系。反应式O表达式要对外来需求作反应。描述反应的公理规定如何反应。有关通讯的公理要求正确的信息被正确的接受者收到。共享变量公理则给出有关共享变量的性质判断。例子用于说明异步顺序O表达式的性质是如何分析的。     

一种基于Petri网的RFID事件检测的形式化方法

无线射频识别(RFID)采用唯一的电子标签识别物理对象,可高速收集大量目标数据.为向各类应用提供语义信息,RFID系统需从收集的数据中检测用户自定义的复合事件.通过提出一种基于Petri网的RFID事件检测方法,引入形式化的ED-net模型描述复合事件语义,并以此为基础实现一种事件检测方法.ED-net模型是对传统Petri网的一种扩展,提供了描述用户自定义类型、函数及表达式的能力,可精确描述RFID复合事件的属性及时域、非时域、参数化等约束条件.通过对RFID事件形式化描述,各种RFID事件可以统一在ED-net模型,并可自动化进行检测处理,避免了不同复合事件间公共子事件重复检测的问题.最后,经过实验测试和分析,验证了该形式化方法的有效性及其优势.     

Solving Inheritance Anomaly with OMNets

This paper presents a concurrent object-oriented modeling language based on Petri nets:OMNets,which hepls greatly to avoid the inheritance anomaly problem appeared in concurrent OO languages.OMNets separates th functional part and the synchroniztion part of objects and uses Petri nets to describe the synchronization part.Both parts are reusable through inheritance.     

从规范到机器代码:通过形式分析构造程序

现代技术将使软件越来越多地固化在硬件之中。有些情况绝对不允许软件中有任何错误,这只是其中一例。因此程序设计必须很快成为一个安全的程序构造过程;也就是说,应把程序设计组织成为进行推理分析的一系列步骤。先用基本谓词逻辑、集合论和代数做工具对问题做细致的形式规范;再以此规范为出发点,应用形式规则导出它的若干算法版本;最后得到面向若干特定具体机器指令系统的程序。真正的程序构造过程自始至终需要严格形式化。包括规范在内的一切版本都可以很方便地用一个程序设计语言表示,该语言包括描述性的以及应用式(applicative)和过程式的各种风格的功能。这样一个语言还要包括非确定性的概念。非确定性使程序开发过程简单明了而且分外灵活,非确定性是由某个做为其基础的抽象数据类型模型解释的。由于使用的是经过形式证明的变换规则,正确性是得到保证的。此外,尽管程序变换方法最初针对的是经典的程序存储式计算机的软件构造,而且现在主要仍用于这类计算机的软件构造,但它可以扩充到其它计算模型,以适应经常提到的硬件体系结构的革新。这些变换规则可以用于任何问题,在这个意义上可以说程序变换是个通用办法。     

新程序设计

在计算机问世以来的几十年中,程序设计经历了从技巧到科学的曲折历程。虽然作为一门科学它的全貌还不全清楚,但人们毕竟已认识到,程序设计应该有它自己的原理和原则的一门科学。在这个方向上迄今取得的成就中,Dijkstra 的贡献是最基本最重要的。     

C.A.Petri与计算机科学

这篇文章是作者在西德GMD(数学和数据处理协会)为庆祝Carl Adam Petri博士六十岁生日召开的会上所作的报告。对Petri的成就和远见卓识作了高度评价。报告观点较高,内容深刻,富有哲理,值得参考。原文系德文,译文系根据Springer-Verlag 1987年出版的书《Cencurrency and Nets》中的英译文译出的。     

死锁的PETRI NETS模型

本文给出了操作系统(OS)的一种基于Petri网的形式化模型,由此把死锁问题转化为线性代数问题。我们得到了OS中死锁存在的充要条件,以及一种消除系统中所有的死锁、保证系统正常工作的最优化方法。特别是对于分布式OS,我们大大改进了以往的一些处理死锁的方法,最后还通过举例进行了说明。     

O-表达式的性质定义与规范

在所提出的程序设计方法中,赋值是物理对象上的操作,而程序则是这种操作的表达式。给出了此类表达式（O-表达式）的安全性和进展性性质的形式化定义,用实例说明了基于这些性质的形式化程序规范的模式。具有明确运行目标的O-表达式称为独立O-表达式（stand-alone O-expression,saloe）。一个完整的程序可能由若干个saloe组成。给出了一个定理,指出如何从这些saloe的性质导出完整性程序的性质。用大量实例阐明了程序性质的形式定义。     

基于UniNet的对象概念研究

This paper discusses concepts on object from UniNet view and shows that there exists the flow of controlin object system except for exchanging of messages between objects. Meanwhile, the paper presents an independent mechanism of object communication separated from object that will result in a more general reuse of object. With helpof the control flow and the data flow, UniNet can describe not only the static features, but also the dynamic featuresof object system, which naturally solve the inheritance anomaly and the flow of data and control. In addition, based on UniNet specification, the object system can be verified easily and create the program code automatically.     

一种新的安全Petri网及其多级安全机制分析

1 引言 Petri网(PN)是一种重要的动态并发系统建模方法,具有因果相关、支持并发、异步和冲突消解等诸多优点,已广泛应用于复杂动态系统建模与仿真验证,例如协议分析、工作流建模、数据库设计等。随着信息安全问题日益突出,迫切需要PN支持多级安全策略的系统建模,使得用PN建立的模型具有良好的多级安全保护机制。但是,现有的PN并不直接支持多级安全系统建模,而且目前对安全PN的研究文献很少。虽然V.Atluri和W.K.Huang等基于着色时间网(CTPN)提出了一种用于多级安全工作流系统建模的安全PN,但他们只考虑了变迁之间的控制安全和时间安全约束,