Translating VDM specifications into ABC programs

Declarative languages such as Miranda and Prolog have often been used to prototype specifications written in the formal notation of VDM, but they have no destructive assignment commands thus making it difficult to model VDM state changes. Imperative languages like C and Pascal allow state changes to be modelled naturally but lack the expressive power to make prototyping feasible. ABC, on the other hand, is a simple yet very powerful imperative language that has a great expressive power making it suitable as a prototyping language. This paper describes the process of translating VDM specifications into ABC programs.     

VDM和Z两种规范描述语言的比较

本文以以关系数据库的规范为例，详细讨论了两种重要的规范描述语言ＶＤＭ和Ｚ的主要区别，对它们的共性和发展史也作了简单介绍。     

基于RUP和VDM++的软件形式化开发方法的研究

形式化方法是软件开发过程中用于保证软件系统具有高度正确性和可靠性的一个重要手段。但形式化软件规范不直观,不容易被开发人员所接受。该文将较为直观地统一软件过程和VDM++形式化方法结合在一起,提出了一种软件形式化开发方法,并通过开发一个实际的文件设备记账系统说明了该方法的可行性与有效性。     

A System for Translating Executable VDM Specifications into Lazy ML

This article describes the process of developing a system for translating VDM executable specifications into Lazy ML prototypes. The system was specified in VDM and a Lazy ML prototype implementation was derived from its specification. This article concentrates on discussing the lessons learned in each stage of the development process, evaluating the adequacy of the used methodology. © 1997 by John Wiley & Sons, Ltd.     

A linearization procedure and a VDM/ECM algorithm for penalized and constrained nonparametric maximum likelihood estimation for mixture models

Suppose independent observations X_i, i=1,…,n are observed from a mixture model , where λ is a scalar and Q(λ) is a nondegenerate distribution with an unspecified form. We consider to estimate Q(λ) by nonparametric maximum likelihood (NPML) method under two scenarios: (1) the likelihood is penalized by a functional g(Q); and (2) Q is under a constraint g(Q)=g₀. We propose a simple and reliable algorithm termed VDM/ECM for Q-estimation when the likelihood is penalized by a linear functional. We show this algorithm can be applied to a more general situation where the penalty is not linear, but a function of linear functionals by a linearization procedure. The constrained NPMLE can be found by penalizing the quadratic distance |g(Q)-g₀|² under a large penalty factor γ>0 using this algorithm. The algorithm is illustrated with two real data sets.     

Parallel-architecture-directed program transformation

The widespread use of parallel machines has been hampered by the difficulty of mapping applications onto them effectively. The difficulty arises because current programming languages require the programmer to specify a problem to be solved at a low level of abstraction in an imperative form. Thus the programmer must immediately encode an architecture-specific algorithm detailing every communication and calculation. This process is prone to error and complicates the reuse of software.

An alternative approach is to specify the problem to be solved at a high-level in a functional language. Meaning-preserving program transformations can then be used to derive a parallel algorithm. Such algorithms can be run on parallel graph-reduction or dataflow machines which automatically exploit the implicit parallelism in a functional language program. Such automatic decomposition techniques, however, are not yet capable of fully yielding the extra performance offered by the parallel hardware.

We show how, by including an architecture specification with the problem specification, and extending the amount of transformation performed, it is possible to produce functional language code that explicity expresses the calculations and communications to be performed by the processors. This simplifies compilation, yields faster programs and enables parallel software to be developed for a wide variety of parallel computer architectures.

A goal-seeking transformation methodology has been developed which enables a high-level functional specification of the problem and a high-level functional abstraction of the target computer architecture to be systematically manipulated to produce an efficient parallel algorithm tailored to the target architecture. As the transformations start from very high-level specifications, the discovery of new algorithms is facilitated.

A case study is used to demonstrate the effectiveness of the technique. We show how a high level specification for sort can be transformed with a pipeline architecture specification to give a mergesort and how the same specification with a dynamic-message-passing architecture specification can be transformed to a novel parallel quicksort.     

基于细胞膜演算的Web服务事务处理形式化描述与验证

采用细胞膜演算具体分析了当前比较主流的Web服务中原子事务协调协议WS-AT．针对WS-AT协议采用简单的状态转换表和转换图,无法描述协调者和多个参与者的复杂协调活动,采用细胞膜演算给出了其形式化描述,用于规范协调者和参与者的活动,并分析了该协议的活性和安全性,得到了38187个状态．模型检验的实验结果表明,该协议满足稳定性、一致性和非平凡性,而不满足非阻塞性．进而,分析出注册和协调协议混在一起是其不满足非阻塞性的原因．     

Specification, Validation, and Synthesis of Email Agent Controllers: A Case Study in Function Rich Reactive System Design

With a few exceptions, previous formal methods for reactive system analysis have focused on finite state machines represented in terms of boolean states and boolean next-state functions. By contrast, in many reactive system domains requirements engineers and developers think in terms of complex data types and expressive next-state functions. Formal methods for reactive system design must be extended to meet their needs as well. I term a reactive system function rich if expressing its state, next-state function, or output function naturally requires this higher expressive power. ISAT, a prototype formal-methods based tool environment, is intended to assist in the creation and validation of function rich reactive systems. This paper describes a case study I have carried out using ISAT to design, validate, synthesize, and evolve controllers for the email agent components making up a novel spam-free email system that I deployed in a user trial in July 1999. The trial has been running since, with high availability, through several evolutionary specification changes and resulting software releases. The case study illustrates the use of a mix of validation techniques, from scenario simulation and coverage through static analysis and theorem proving, and discusses the value each technique adds. In addition to summarizing ISAT and the trial, this paper discusses tool requirements placed by the domain and task, the simple and powerful platform/controller/pure-functions software architecture of the components, and lessons learned.     

HB协议的形式规约与验证

形式化方法是确保安全协议设计正确性的重要工具,利用形式化方法已经发现了许多安全协议的设计错误.首次利用形式规约语言Z对RFID安全协议HB进行形式规约, 并对HB协议应该满足的安全性质进行形式化描述,使用Z模式推理从协议及其运行环境两个方面验证了协议的关键安全属性,发现了HB协议在设计方面的缺陷,提出了HB协议的一种改进方法.     

Automated Synthesis of Numerical Programs for Simulation of Rigid Mechanical Systems in Physics-Based Animation

Physics-based animation programs are important in a variety of contexts, including science, engineering, education and entertainment among others. Manual construction of such programs is expensive, time-consuming and prone to error. We have developed a system for automatically synthesizing physics-based animation programs for a significant class of problems: constrained systems of rigid bodies, subject to driving and dissipative forces, under the control of an interactive user. Our system includes a graphical interface for specifying a physical scenario, including objects, geometry and coordinate systems, along with a symbolic interface for specifying dynamical variables, forces and constraints operating in the scenario. The entities defined in the graphical interface serve as the underlying vocabulary for specifications entered in the symbolic interface. Our system partitions the constraints and dynamical variables into classes and assigns each class to be implemented in a different component of a general simulation program scheme. It generates a numerical C⁺⁺ simulation program that drives a real-time animation of the specified scenario. Our system is implemented as a collection of rewrite rules in the Mathematica programming language. Our approach provides some of the benefits of formal deductive program synthesis, while keeping the computational costs of program synthesis more in line with conventional program generator technology. We have successfully tested our system on numerous examples.     

基于重写逻辑的Web服务事务处理形式化描述

Web服务的事务处理研究越来越活跃,对于Web服务中的长、短事务进行形式化描述与验证是很重要的,但目前还没有成熟的方法．该文提出了一种基于重写逻辑的Web服务事务处理形式化描述方法,采用重写逻辑工具Maude,对于描述Web事务的细胞膜演算,给出一个事务处理的通用框架,采用重写逻辑中的规则描述事务的具体活动,并且引入事务补偿机制刻画长事务的运行;并应用该模型形式化描述文中的Web事务经典例子,得到一个可执行的重写逻辑模型,便于以后采用Maude线性时序逻辑分析器进行形式化分析．     

Theorem Proving Guided Development of Formal Assertions in a Resource-Constrained Scheduler for High-Level Synthesis

This paper presents a formal specification and a proof of correctness for the widely-used Force-Directed List Scheduling (FDLS) algorithm for resource-constrained scheduling of data flow graphs in high-level synthesis systems. The proof effort is conducted using a higher-order logic theorem prover. During the proof effort many interesting properties of the FDLS algorithm are discovered. These properties are formally stated and proved in a higher-order logic theorem proving environment. These properties constitute a detailed set of formal assertions and invariants that should hold at various steps in the FDLS algorithm. They are then inserted as programming assertions in the implementation of the FDLS algorithm in a production-strength high-level synthesis system. When turned on, the programming assertions (1) certify whether a specific run of the FDLS algorithm produced correct schedules and, (2) in the event of failure, help discover and isolate programming errors in the FDLS implementation.We present a detailed example and several experiments to demonstrate the effectiveness of these assertions in discovering and isolating errors. Based on this experience, we discuss the role of the formal theorem proving exercise in developing a useful set of assertions for embedding in the scheduler code and argue that in the absence of such a formal proof checking effort, discovering such a useful set of assertions would have been an arduous if not impossible task.     

Planning Proofs of Equations in CCS

Most efforts to automate formal verification of communicating systems have centred around finite-state systems (FSSs). However, FSSs are incapable of modelling many practical communicating systems, including a novel class of problems, which we call VIPS. VIPSs are value-passing, infinite-state, parameterised systems. Existing approaches using model checking over FSSs are insufficient for VIPSs. This is due to their inability both to reason with and about domain-specific theories, and to cope with systems having an unbounded or arbitrary state space.We use the Calculus of Communicating Systems (CCS) (Communication and Concurrency. London: Prentice Hall, 1989) to express and specify VIPSs. We take program verification to be proving the program and its intended specification equivalent. We use the laws of CCS to conduct the verification task. This approach allows us to study communicating systems and the data such systems communicate. Automating theorem proving in this context is an extremely difficult task.We provide automated methods for CCS analysis; they are applicable to both FSSs and VIPSs. Adding these methods to the CL ^A M proof planner (Lecture Notes in Artificial Intelligence, Vol. 449, Springer, 1990, pp. 647, 648), we have implemented an automated verification planner capable of dealing with problems that previously required human interaction. This paper describes these methods, gives an account as to why they work, and provides a short summary of experimental results.     

A Compositional Behavioral Modeling Framework for Embedded System Design and Conformance Checking

We propose a framework based on a synchronous multi-clocked model of computation to support the inductive and compositional construction of scalable behavioral models of embedded systems engineered with de facto standard design and programming languages. Behavioral modeling is seen under the paradigm of type inference. The aim of the proposed type system is to capture the behavior of a system under design and to re-factor it by performing global optimizing and architecture-sensitive transformations on it. It allows to modularly express a wide spectrum of static and dynamic behavioral properties and automatically or manually scale the desired degree of abstraction of these properties for efficient verification. The type system is presented using a generic and language-independent static single assignment intermediate representation.     

安全协议的形式化说明、设计及验证

文中针对形式化技术在安全协议说明、设计和验证三个方面的研究和进展情况进行了详细介绍,分析了它们的原理和优缺点,并对该技术的研究发展前景提出见解。