A graph-based generic type system for object-oriented programs

We present a graph-basedmodel of a generic type system for an OO language. The type system supports the features of recursive types, generics and interfaces, which are commonly found in modern OO languages such as Java. In the classical graph theory, we define type graphs, instantiation graphs and conjunction graphs that naturally illustrate the relations among types, generics and interfaces within complex OO programs. The model employs a combination of nominal and anonymous nodes to represent respectively types that are identified by names and structures, and defines graph-based relations and operations on types including equivalence, subtyping, conjunction and instantiation. Algorithms based on the graph structures are designed for the implementation of the type system. We believe that this type system is important for the development of a graph-based logical foundation of a formal method for verification of and reasoning about OO programs.     

一类递归函数的多态类型

以上下文无关语言上的递归函数为基础的语言LFC(1anguage for context free recursive function)是一种形式规约语言,适于处理短语结构.LFC也是函数式语言,具有函数式语言的许多特点.LFC已经在形式规约获取系统SAQ(specification acquisition system)中实现,为其最初设计的类型系统不支持多态类型.引入类型变量和相应的类型检查方法,就可以将其类型系统扩充为多态类型系统.对多态类型系统实现中的一些问题也进行了讨论.在实现多态之后,LFC     

一种包解析器硬件配置描述语言及其编译结构

本文设计一种用于实现可重构网络数据包解析器的专用硬件配置描述语言P3.由于要有利于高安全等级网络的实现,我们侧重于从高可信性角度进行语言设计,包括形式化定义该语言的类型系统和操作语义,以及设计其可信编译结构.基于对可重构硬件基本需求的充分理解,本文从软硬件协同角度出发,最终明确了P3语言的核心特性及其编译器P3C的可信编译结构.由于可重构数据包解析器是软件定义网络（SDN）、可编程数据平面的重要一环,因此实现P3C的可信编译结构将对SDN的安全性有着重大意义.期待P3C项目的开展,能促进网络与形式化领域相关工作的进一步研究.     

A Type System for the Java Bytecode Language and Verifier

The Java Virtual Machine executes bytecode programs that may have been sent from other, possibly untrusted, locations on the network. Since the transmitted code may be written by a malicious party or corrupted during network transmission, the Java Virtual Machine contains a bytecode verifier to check the code for type errors before it is run. As illustrated by reported attacks on Java run-time systems, the verifier is essential for system security. However, no formal specification of the bytecode verifier exists in the Java Virtual Machine Specification published by Sun. In this paper, we develop such a specification in the form of a type system for a subset of the bytecode language. The subset includes classes, interfaces, constructors, methods, exceptions, and bytecode subroutines. We also present a type checking algorithm and prototype bytecode verifier implementation, and we conclude by discussing other applications of this work. For example, we show how to extend our formal system to check other program properties, such as the correct use of object locks. This revised version was published online in August 2006 with corrections to the Cover Date.     

Feedback linearization and linear observer for a quadrotor unmanned aerial vehicle

The paper gives the answer to the question formulated in the title for the case of manipulator-level languages [1]. Theoretical considerations show that regardless of the type and number of robots and cooperating devices used in the system as well as irrespective of the number and kind of sensors included in the system, a general purpose language has to be extended by a single instruction with a rather complex semantics. Due to this complexity it is more convenient to introduce two, much simpler instructions. The paper also presents the method of implementing those instructions in a hierarchical distributed control system. The presented approach has been used in the implementation of MRROC/MRROC++ robot programming libraries/languages. The programmer uses predefined library modules to construct the controller structure solving a specific multi-robot task. The structure is fine-tuned to the task at hand by supplying adequate motion generators in a plug-in fashion. The practical validity of the formal approach followed in the implementation of MRROC and MRROC++ has been positively verified on diverse robotic tasks.     

基于Z语言的电信服务系统的形式化规格

形式化方法是基于数学的系统开发方法,它可以应用于系统开发的各个阶段,包括系统需求、设计、实现、测试等。首先介绍了形式化规格语言Z,接着用Z开发电信服务系统的形式化规格,并对形式化规格进行验证,以期提高电信服务系统的稳定性,也为探测电信服务系统的功能冲突、预防系统缺陷的产生提供研究的基础和支持。     

Molecule: a language construct for layered development of parallelprograms

A new language construct, called molecule, is described for the efficient implementation of algorithms on parallel computers. A molecule can be considered a procedure associated with a molecule type. Each molecule type characterizes a particular computation mode (sequential, pipelining, array processing, dataflow, multiprocessing, etc.). Basic concepts of molecule are introduced with a procedural language, called PAL. A concrete example is presented to illustrate layered software development using PAL on a multicomputer (the iPSC). It is concluded that high-level languages, augmented with the molecule construct, offer application flexibility, user friendliness, and efficiency in implementing parallel programs     

命令的操作语义在类型系统中的一种表示

类型系统建立在一个小的规则集合基础上，易于实现，可理解性好，且具有计算完全性和足够的表达能力,在类型系统中可以重述推导规则，将其形式化为一些归纳关系，从而直接表示了命令的操作语义,类型理论不仅适合于函数式程序的证明，也是刻画和证明命令式程序的合适的框架。     

服务组合的代数规约

现有的服务组合描述途径不能有效地验证和测试组合正确性,针对这一问题,提出了一个代数规约方法,引入规约包机制扩展面向服务代数规约语言SOFIA以支持该方法。用代数规约单元描述服务系统中的各种实体,其中基调部分定义实体的语法和结构,公理部分定义其功能和行为特性。与一个服务相关的规约单元封装在一个包中或拆分在几个相互引用的包中,每个包形成一个命名空间。当多个服务组合在一起时,以这些服务的代数规约包为基础,一方面抽象地定义组合服务的交互过程和语义,形成描述服务组合实现方式的实现规约包;另一方面抽象地定义组合服务对外接口及其功能语义,形成描述组合服务需求的抽象规约包。在实现规约和抽象规约的双元结构基础上,进一步定义了实现规约和抽象规约之间必须满足的“实现”关系,证明了满足实现关系可以保证实现的正确性,从而为服务组合的可验证性和可测试性奠定了理论基础。最后结合实例分析阐述了用代数规约描述服务组合的抽象性、可表达性和可验证性。     

Integrating a formal method into a software engineering process with UML and Java

We describe how CSP-OZ, a formal method combining the process algebra CSP with the specification language Object-Z, can be integrated into an object-oriented software engineering process employing the UML as a modelling and Java as an implementation language. The benefit of this integration lies in the rigour of the formal method, which improves the precision of the constructed models and opens up the possibility of (1) verifying properties of models in the early design phases, and (2) checking adherence of implementations to models. The envisaged application area of our approach is the design of distributed reactive systems. To this end, we propose a specific UML profile for reactive systems. The profile contains facilities for modelling components, their interfaces and interconnections via synchronous/broadcast communication, and the overall architecture of a system. The integration with the formal method proceeds by generating a significant part of the CSP-OZ specification from the initially developed UML model. The formal specification is on the one hand the starting point for verifying properties of the model, for instance by using the FDR model checker. On the other hand, it is the basis for generating contracts for the final implementation. Contracts are written in the Java Modeling Language (JML) complemented by CSP_jassda, an assertion language for specifying orderings between method invocations. A set of tools for runtime checking can be used to supervise the adherence of the final Java implementation to the generated contracts. This research was partially supported by the DFG project ForMooS (grants OL 98/3-2 and WE 2290/5-1). C. B. Jones     

Language definition-based compiler development

An important reason for developing a formal definition of a programming language is to provide guidance for implementors. At the very least, a formal definition establishes a standard of implementation correctness. Here we examine one avenue of compiler implementation based on a constructive functional language definition organized into a set of modular theories and syntax-directed rules. A modular implementation, whose structure follows that of the formal definition, is developed by a combination of hand coding and semiformal transformations that bring the definition down to the level of a program in a Pascal-like language. Program verification techniques are then used to confirm the correctness of the implementation steps.     

General test result checking with log file analysis

We describe and apply a lightweight formal method for checking test results. The method assumes that the software under test writes a text log file; this log file is then analyzed by a program to see if it reveals failures. We suggest a state-machine-based formalism for specifying the log file analyzer programs and describe a language and implementation based on that formalism. We report on empirical studies of the application of log file analysis to random testing of units. We describe the results of experiments done to compare the performance and effectiveness of random unit testing with coverage checking and log file analysis to other unit testing procedures. The experiments suggest that writing a formal log file analyzer and using random testing is competitive with other formal and informal methods for unit testing.     

C程序类型隐式转换漏洞的静态检测

C语言由于其灵活性及支持环境,经常被用于嵌入式和实时开发环境中,所以它已成为一种非常流行的语言。但凡事都有两面性,C语言在提供了很大灵活性的同时也存在不少安全隐患。该文主要讨论C源程序中类型隐式转换导致程序错误的常见表现形式,分析其特征及产生机理,从而提出一种以语法制导翻译的方式形式化描述漏洞,并且给出了其实现方法。     

Formal verification of Ada programs

The Penelope verification editor and its formal basis are described. Penelope is a prototype system for the interactive development and verification of programs that are written in a rich subset of sequential Ada. Because it generates verification conditions incrementally, Penelope can be used to develop a program and its correctness proof in concert. If an already-verified program is modified, one can attempt to prove the modified version by replaying and modifying the original sequence of proof steps. Verification conditions are generated by predicate transformers whose logical soundness can be proven by establishing a precise formal connection between predicate transformation and denotational definitions in the style of continuation semantics. Penelope's specification language, Larch/Ada, belongs to the family of Larch interface languages. It scales up properly, in the sense that one can demonstrate the soundness of decomposing an implementation hierarchically and reasoning locally about the implementation of each node in the hierarchy     

Signatures: A language extension for improving type abstraction and subtype polymorphism in C++

C++ uses inheritance as a substitute for subtype polymorphism. We give examples where this makes the type system too inflexible. We then describe a conservative language extension that allows a programmer to define an abstract type hierarchy independent of any implementation hierarchies, to retroactively abstract over an implementation, and to decouple subtyping from inheritance. This extension gives the user more of the flexibility of dynamic typing while retaining the efficiency and security of static typing. With default implementations and views flexible mechanisms are provided for implementing an abstract type by different concrete class types. We first show how the language extension can be implemented in a preprocessor to a C++ compiler, and then detail and analyse the efficiency of an implementation we directly incorporated in the GNU C++ compiler.     

A verified Common Lisp implementation of Buchberger’s algorithm in ACL2

In this article, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in ACL2, a system which provides an integrated environment where programming (in a pure functional subset of Common Lisp) and formal verification of programs, with the assistance of a theorem prover, are possible. Our implementation is written in a real programming language and it is directly executable within the ACL2 system or any compliant Common Lisp system. We provide here snippets of real verified code, discuss the formalization details in depth, and present quantitative data about the proof effort.     

一种用于Java程序验证编译的标签类型

在基于语言考虑代码安全性的工作中,往往需要将高级语言程序翻译成类型化低级语言的程序进行类型检查.许多高级语言具有类型调度结构,在向低级语言的编译过程中需要用标签机制来实现.针对具有多继承接口的Java程序包含的一种特殊的类型调度结构,提出了一种新的标签类型.包含这种标签类型的低级语言能够有效地实现Java程序中的接口调用.这种对接口调用的编译方法被用在一个以类型化低级语言为验证语言的Java字节码即时编译器中.     

一种形式化的基于TTCN的测试执行方法

探讨基于形式化技术的测试执行方法是开展形式化的协议一致性测试活动的关键环节．本文提出了一种形式化的基于测试描述语言ＴＴＣＮ的操作语义的测试执行方法，并使用标号变迁系统刻画了这一方法的整个执行过程，同时讨论了这个方法的一个具体实现．这种形式化的基于ＴＴＣＮ的测试执行方法非常适合于构造通用的协议测试系统，同时也是进行测试集的自动验证的有效手段.     

Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation

With the explosion of software size, checking conformance of implementation to specification becomes an increasingly important but also hard problem. Current practice based on ad-hoc testing does not provide correctness guarantees, while highly confident traditional formal methods like model checking and theorem proving are still too expensive to become common practice. In this paper we present a paradigm for combining formal specification with implementation, called monitoring-oriented programming (MoP), providing a light-weighted formal method to check conformance of implementation to specification at runtime. System requirements are expressed using formal specifications given as annotations inserted at various user selected places in programs. Efficient monitoring code using the same target language as the implementation is then automatically generated during a pre-compilation stage. The generated code has the same effect as a logical checking of requirements and can be used in any context, in particular to trigger user defined actions, when requirements are violated. Our proposal is language- and logic- independent, and we argue that it smoothly integrates other interesting system development paradigms, such as design by contract and aspect oriented programming. A prototype has been implemented for Java, which currently supports requirements expressed using past time and future time linear temporal logics, as well as extended regular expressions.