RESEARCH INITIATION AWARD: Executable Specifications for the Design of Object-Oriented Systems

可执行规范被认为是软件系统设计的重要支持工具，因为它集成了形式化分析的方法，以及在软件生命周期的早期阶段对系统设计进行分析和验证的更具实验性的原型和测试方法。然而，可执行规范在面向对象研究中仍然是一个处女地。本研究的动机是为了弥补当前面向对象研究中这一重要的技术差距。研究面向对象系统的可执行设计规范语言。这种语言被称为扩展G- nets (eG-Nets)，它是基于Petri网理论和PI之前在G-Net框架上的工作。eG-Net的设计代表了软件规范的模块化方法，因为eG-Net规范不仅指定了面向对象系统的行为，而且还指定了设计的结构。EG-Net规范在分布式环境下可直接执行。

Executable specification is regarded as an important supporting tool for software system design, because it integrates the method of formal analysis, and the more experimental approach of prototyping and testing to analyze and to verify the design of a system at early stage of the software life cycle. However, executable specification is still a virgin area in OO research. The motivation of this research is to bridge this important technological gap in the current OO research. An executable design specification language for OO systems will be studied. The language is called extended G-Nets (eG-Nets), which is based on the theory of Petri nets, and the PI's previous work on the G- Net framework. The design of eG-Nets represents a modular approach for software specifications in the sense that an eG- Net specification not only specifies the behavior of an OO system, but also the structure of the design. EG-Net specifications are directly executable in distributed environment.