互逆主义程序精化——程序精化从形式化到半自动化的发展

Carroll Morgan的规则精化方法是一种典型的程序精化方法,是一种形式方法.本文用互逆主义逻辑对其进行了改造将其中的精化法则改造成为逻辑定理,以二层假言推理和小前提逆二层单准正向证明系统为推理规则,使得程序精化从形式化发展为半自动化.     

Huffman算法程序的形式化推导

使用PAR方法形式化推导了解决最优编码问题的Huffman算法。推导过程充分利用最优编码树的特性,在对原问题进行分划归约为子问题时,引入一个新元素来取代原来的2个或多个元素,使用一套接近数学语言的抽象记号表示集合、二叉树等,推导过程简洁且能生成正确的算法。该Huffman算法能在PAR平台上通过自动生成系统转换成可执行语言程序,并正常运行。     

Formal Program Verification Using Symbolic Execution

Symbolic execution provides a mechanism for formally proving programs correct. A notation is introduced which allows a concise presentation of rules of inference based on symbolic execution. Using this notation, rules of inference are developed to handle a number of language features, including loops and procedures with multiple exits. An attribute grammar is used to formally describe symbolic expression evaluation, and the treatment of function calls with side effects is shown to be straightforward. Because symbolic execution is related to program interpretation, it is an easy-to-comprehend, yet powerful technique. The rules of inference are useful in expressing the semantics of a language and form the basis of a mechanical verification condition generator.     

Program Development Schemata as Derived Rules

We show how the formalization and application of schemata for program development can be reduced to the formalization and application of derived rules of inference. We formalize and derive schemata as rules in theories that axiomatize program data and programs themselves. We reduce schema-based program development to ordinary theorem proving, where higher-order unification is used to apply rules. Conceptually, our formalization is simple and unifies divergent views of schemata, program synthesis, and program transformation. Practically, our formalization yields a simple methodology for carrying out development using existing logical frameworks; we illustrate this in the domain of logic program synthesis and transformation using the Isabelle logical framework.     

Program Synthesis from Formal Requirements Specifications Using APTS

Formal specifications of software systems are extremely useful because they can be rigorously analyzed, verified, and validated, giving high confidence that the specification captures the desired behavior. To transfer this confidence to the actual source code implementation, a formal link is needed between the specification and the implementation. Generating the implementation directly from the specification provides one such link. A program transformation system such as Paige's APTS can be useful in developing a source code generator. This paper describes a case study in which APTS was used to produce code generators that construct C source code from a requirements specification in the SCR (Software Cost Reduction) tabular notation. In the study, two different code generation strategies were explored. The first strategy uses rewrite rules to transform the parse tree of an SCR specification into a parse tree for the corresponding C code. The second strategy associates a relation with each node of the specification parse tree. Each member of this relation acts as an attribute, holding the C code corresponding to the tree at the associated node; the root of the tree has the entire C program as its member of the relation. This paper describes the two code generators supported by APTS, how each was used to synthesize code for two example SCR requirements specifications, and what was learned about APTS from these implementations.     

形式化方法B及其程序规约机理

用形式化方法开发软件是提高软件可靠性和生产效率的革命性途径,是实现软件自动化的关键。文章针对B方法,介绍了其产生的历史背景,分析了其程序规约机理,并结合实例给出了B方法中抽象机的具体运用,对该方法的特点进行了评述。     

Information Systems Development as an Activity

Information systems development (ISD) is analysed in this paper as asystemic work activity, using Activity Analysis and Development (ActAD)as the theoretical framework. ISD is regarded here as the process bywhich some collective work activity is facilitated by newinformation-technological means through analysis, design, implementation,introduction and sustained support, as well as process management. Itis a temporary, boundary-crossing activity which draws its actors,means, rules, etc. from two sides – typically a software companyand the IS user organization. ISD is analysed as a part of a networkof activities, too, around software development and a computer-supporteduse activity. A theoretical framework and a pragmatic checklist arepresented for studying ISD activities. It is argued that the activity-theoretical framework provides a theoretically foundedbut detailed and practicable procedure for studying ISD as a workactivity in context.     

UML实时活动图的形式化分析

统一建模语言(UML)自从成为OMG规范后,应用越来越广泛．但UML没有精确的、形式化的语义阻碍了它的进一步发展．该文基于Petri网,给出带时间约束的UML活动图的形式化描述．与Petri网不同的是,Petri网的时间约束是在跃迁(transition)上,而作者将UML活动图的时间约束放在活动状态上,在此基础上,用整型时间的验证技术对实时活动图的时间性质加以分析,为实时系统的建模打下了基础.     

Exception Handling: Formal Specification and Systematic Program Construction

We present an algebraic specification language (PLUSS) and a program construction method. Programs are built systematically from an algebraic specification of the data they deal with. The method was tested on a realistic problem (part of a telephone switching system). In these experiments, it turned out that error handling was the difficult part to specify and to program. This paper shows how to cope with this problem at the specification level and during the program development process.     

Towards a Formal Basis for the Formal Development Method and the Ina Jo Specification Language

In carrying out SDC's Formal Development Method, one writes a specification of a system under design in the Ina Jo™ specification language and proves that the specification meets the requirements of the system. This paper develops an abstract machine model of what is specified by a level specification in an Ina Jo specification. It describes the state as defined by the front matter, computations as defined by initial states and transforms, and invariants, criteria, and constraints as properties of computations. The paper then describes a number of formal design methods and the kinds of abstractions that they require. For each of these kinds of abstractions, there is a characteristic relationship between refinements that should be proved as one is carrying out the method.     

Coordination as a Service: Ontological and Formal Foundation

Coordination models like Lindawere first conceived in the context of closed systemslike high-performance parallel applications  where all coordinated entities were known once and for all at design time, and coordination media were conceptually part of a coordinated application. Correspondingly, traditional formalisations of coordination models  where both coordinated entities and coordination media are uniformly represented as terms of a process algebra  endorse the viewpoint of coordination as a language for building concurrent systems.Today, new application scenarios call for a new approach to the formalisation of coordination models and systems. The complexity of today systems requires coordination media to be seen as first-class design abstractions, affecting the engineering process down to the deployment of infrastructures providing coordination services, for which effectiveness and reliability may be critical properties demanding a formal treatment.As a unifying framework for a number of existing works on the semantics of coordination media, in this paper we present a basic ontology and a formal framework endorsing the viewpoint of coordination as a service. Typical process algebra techniques are here exploited to represent the semantics of a coordinated system in terms of the interactive behaviour of coordination media. By this framework, coordination media are seen as primary abstractions amenable of formal investigation, promoting their exploitation at any step of the engineering process.     

软件开发的形式化方法

随着计算机及软件系统逐步渗透到社会生活的方方面面,对软件可靠性、安全性和保密性的要求也越来越高．本文阐述了形式化方法的定义、重要性及主要研究内容。着重讨论了形式规约方法,以及演绎证明和模型检测等形式验证方法。     

基于PAR的算法形式化开发

形式化方法是构建可信软件的重要途径.基于对算法问题的分析,针对形式化方法PAR开发算法的特征,刻划了问题分划、递推关系构造方面的规律.从一类问题的形式化功能规约出发,可机械地完成问题的分划及规约的变换,自然地揭示出求解问题的算法思想,在相关工具的支持下自动生成算法程序.研究结果将算法设计中尽可能多的创造性劳动转化为非创造性劳动,降低了形式化求解算法问题的难度,提高了算法程序的可靠性和形式化开发效率.     

Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations

This article presents the formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C and compiler intermediate languages. Beyond giving semantics to pointer-based programs, this model supports reasoning over transformations of such programs. We show how the properties of the memory model are used to prove semantic preservation for three passes of the Compcert verified compiler.     

一种基于模糊形式概念分析的程序聚类方法

程序聚类通过将与同一个需求或设计元素相关的代码单元聚集在一起来辅助程序理解及系统结构分析.其中,形式概念分析(FCA)是一类被广泛采用的程序聚类技术.然而现有基于FCA的程序聚类方法都是基于二值属性构建的,无法处理模糊信息.提出将模糊概念分析用于基于文本分析的程序聚类,提出了一种支持模糊信息的程序聚类方法.该方法包括模糊属性的采集过程以及相应的模糊概念格的构造算法.在此基础上,开发了一个半自动化的程序分析工具,并将其应用到一个商业软件分析中.初步的实验结果表明该方法能够有效地支持基于模糊特征的程序聚类,对于提高遗留系统的维护效率有明显的帮助.     

静态程序分析过程中形式化验证工具Frama-C的应用

软件的静态程序分析是确保软件安全可靠的一种有效手段。常见的形式化的静态分析工具一般是基于模型检测,定理证明或抽象解释理论来对软件进行分析验证。然而,基于单一理论的验证工具具有一定的局限性。介绍了一个开源的静态分析平台Frama-C,根据该工具的特点,分别使用不同的插件对一小段代码进行静态分析,有助于将不同的程序分析方法相结合。最后对如何使用Frama-C工具解决航空控制软件等安全关键软件的执行时间分析问题的过程进行了演示。