A Program Refinement Tool

The refinement calculus for the development of programs from specifications is well suited to mechanised support. We review the requirements for tool support of refinement as gleaned from our experience with existing refinement tools, and report on the design and implementation of a new tool to support refinement based on these requirements. The main features of the new tool are close integration of refinement and proof in a single tool (the same mechanism is used for both), good management of the refinement context, an extensible theory base that allows the tool to be adapted to new application domains, and a flexible user interface. Received June 1997 / Accepted in revised form June 1998     

Structured mesh generation by kriging with local refinement with a new elliptic scheme

Accurate results in finite element analysis are strongly related to mesh quality. In this paper, an automatic quadrilateral mesh generation methodology using kriging interpolation is described, a quality mesh study is conducted, and the development of a new local refinement scheme, called the elliptic scheme, is presented. The new elliptic refinement scheme is evaluated using four standard structural cases, and it is shown that it compares very well with octree-based refinement schemes and other local refinement methods.     

A comparison of refinement orderings and their associated simulation rules

In this paper we compare the refinement orderings, and their associated simulation rules, of state-based specification languages such as Z and Object-Z with the refinement orderings of event-based specification languages such as CSP. We prove with a simple counter-example that data refinement, established using the standard simulation rules for Z, does not imply failures refinement in CSP. This contradicts accepted results.Having explored the differences between the simulation rules for establishing data refinement and those for establishing the refinement of action systems and state-transition systems—models in which refinement is equivalent to failures refinement within CSP—we present a new set of simulation rules for data types. These alternative rules are both sound and jointly complete with respect to the stable failures refinement ordering. Furthermore we present an alternative refinement ordering for CSP, one in which refinement is equivalent to data refinement in Z.     

Refinement patterns for ASTDs

This paper introduces three refinement patterns for algebraic state-transition diagrams (astds): state refinement, transition refinement and loop-transition refinement. These refinement patterns are derived from practice in using astds for specifying information systems and security policies in two industrial research projects. Two refinement relations used in these patterns are formally defined. For each pattern, proof obligations are proposed to ensure preservation of behaviour through refinement. The proposed refinement relations essentially consist in preserving scenarios by replacing abstract events with concrete events, or by introducing new events. Deadlocks cannot be introduced; divergence over new events is allowed in one of the refinement relation. We prove congruence-like properties for these three patterns, in order to show that they can be applied to a subpart of a specification while preserving global properties. These three refinement patterns are illustrated with a simple case study of a complaint management system.     

A consistent octree hanging node elimination algorithm for hexahedral mesh generation

A new algorithm for hanging node elimination in octree structures is developed. The proposed algorithm utilizes hanging node elimination by refinement templates and a new mesh conditioning technique based on decoupling templates. Refinement templates insert transition elements to eliminate hanging nodes. Decoupling templates insert circular loops in the dual mesh without introducing or removing hanging nodes. Decoupling templates are introduced to avoid full refinement in the cases that do not match any of the available refinement templates. The proposed algorithm eliminates hanging nodes for concavely refined regions without excessive refinement. Another advantage of the proposed algorithm lies in eliminating narrow gaps of coarse meshes between refined regions. This step has a positive effect on the mesh quality as it avoids introducing non-regular templates with a limited penalty of uniform refinement. The presented algorithm produces good quality meshes and provides a consistent and complete method for producing conformally refined octree structures.     

Laws of data refinement

Summary A specification language typically contains sophisticated data types that are expensive or even impossible to implement. Their replacement with simpler or more efficiently implementable types during the programming process is called data refinement. We give a new formal definiton of data refinement and use it to derive some basic laws. The derived laws are constructive in that used in conjunction with the known laws of procedural refinement they allow us to calculate a new specification from a given one in which variables are to be replaced by other variables of a different type.     

Taking Decisions Late: End-Based Choice Combined with Action Refinement

A choice in concurrent systems is usually taken by the starting of an action. We propose the alternative view that a choice is determined by the ending of actions as this alternative has relevant applications and interesting implications. The different points of view lead in particular to different refinement operators.We introduce a refinement operator on bundle event structures for the end-based view. The standard equivalences are not preserved by this refinement operator. Therefore, we also introduce and study new equivalences that are preserved by our refinement operator.     

Towards practical anisotropic adaptive FEM on triangular meshes: a new refinement paradigm

Adaptive anisotropic refinement of finite element meshes allows one to reduce the computational effort required to achieve a specified accuracy of the solution of a PDE problem. We present a new approach to adaptive refinement and demonstrate that this allows one to construct algorithms which generate very flexible and efficient anisotropically refined meshes, even improving the convergence order compared to adaptive isotropic refinement if the problem permits.     

A framework for automated and certified refinement steps

The refinement calculus provides a methodology for transforming an abstract specification into a concrete implementation, by following a succession of refinement rules. These rules have been mechanized in theorem provers, thus providing a formal and rigorous way to prove that a given program refines another one. In a previous work, we have extended this mechanization for object-oriented programs, where the memory is represented as a graph, and we have integrated our approach within the rCOS tool, a model-driven software development tool providing a refinement language. Hence, for any refinement step, the tool automatically generates the corresponding proof obligations and the user can manually discharge them, using a provided library of refinement lemmas. In this work, we propose an approach to automate the search of possible refinement rules from a program to another, using the rewriting tool Maude. Each refinement rule in Maude is associated with the corresponding lemma in Isabelle, thus allowing the tool to automatically generate the Isabelle proof when a refinement rule can be automatically found. The user can add a new refinement rule by providing the corresponding Maude rule and Isabelle lemma.     

A new scheme for mesh generation and mesh refinement using graph theory

There are an extensive number of algorithms available from graph theory, some of which, for problems with geometric content, make graphs an attractive framework in which to model an object from its geometry to its discretization into a finite element mesh. This paper presents a new scheme for finite element mesh generation and mesh refinement using concepts from graph theory. This new technique, which is suitable for an interactive graphical environment, can also be used efficiently for fully automatic remeshing in association with self-adaptive schemes. Problems of mesh refinement around holes and local mesh refinement are treated. The suitability of the algorithms presented in this paper is demonstrated by some examples.     

Counterexample-guided abstraction refinement for linear programs with arrays

Predicate abstraction refinement is one of the leading approaches to software verification. The key idea is to abstract the input program into a Boolean Program (i.e. a program whose variables range over the Boolean values only and model the truth values of predicates corresponding to properties of the program state), and refinement searches for new predicates in order to build a new, more refined abstraction. Thus Boolean programs are commonly employed as a simple, yet useful abstraction. However, the effectiveness of predicate abstraction refinement on programs that involve a tight interplay between data-flow and control-flow is still to be ascertained. We present a novel counterexample guided abstraction refinement procedure for Linear Programs with arrays, a fragment of the C programming language where variables and array elements range over a numeric domain and expressions involve linear combinations of variables and array elements. In our procedure the input program is abstracted w.r.t. a family of sets of array indices, the abstraction is a Linear Program (without arrays), and refinement searches for new array indices. We use Linear Programs as the target of the abstraction (instead of Boolean programs) as they allow to express complex correlations between data and control. Thus, unlike the approaches based on predicate abstraction, our approach treats arrays precisely. This is an important feature as arrays are ubiquitous in programming. We provide a precise account of the abstraction, Model Checking, and refinement processes, discuss their implementation in the EUREKA tool, and present a detailed analysis of the experimental results confirming the effectiveness of our approach on a number of programs of interest.     

Breaking the Model: Finalisation and a Taxonomy of Security Attacks

It is well known that security properties are not preserved by refinement, and that refinement can introduce new, covert, channels, such as timing channels. The finalisation step in refinement can be analysed to identify some of these channels, as unwanted finalisations that can break the assumptions of the formal model. We introduce a taxonomy of such unwanted finalisations, and give examples of attacks that exploit them.     

Introducing extra operations in refinement

This paper reconsiders refinements which introduce actions on the concrete level which were not present at the abstract level. It considers a range of different basic refinement relations, covering the standard ones for formalisms like Event-B, Z, action systems, and CSP. It also describes a number of ways in which new operations may be introduced: extended interfaces, internal actions, stuttering steps, and action refinement. The main contribution of this paper is in exploring the interaction between those two dimensions. In particular, it shows how the “refining skip” method is incompatible with failures-based refinement relations, and consequently some decisions in designing Event-B refinement are more entangled than previously highlighted.     

Foundations for using linear temporal logic in Event-B refinement

In this paper we present a new way of reconciling Event-B refinement with linear temporal logic (LTL) properties. In particular, the results presented in this paper allow properties to be established for abstract system models, and identify conditions to ensure that the properties (suitably translated) continue to hold as those models are developed through refinement. There are several novel elements to this achievement: (1) we identify conditions that allow LTL properties to be mapped across refinement chains; (2) we provide translations of LTL predicates to reflect the introduction through refinement of new events and the renaming and splitting of existing events; (3) we do this for an extended version of LTL particularly suited to Event-B, including state predicates and enabledness of events, which can be model-checked at the abstract level. Our results are more general than any previous work in this area, covering liveness in the context of anticipated events, and relaxing constraints between adjacent refinement levels. The approach is illustrated with a case study. This enables designers to develop event based models and to consider their execution patterns so that liveness and fairness properties can be verified for Event-B systems.     

基于UML和Z的软件体系结构求精方法及其应用

论文探讨了如何将可视化建模语言UML和形式化描述语言Z集成而得到一种新的求精方法,寻求一种在软件体系结构求精过程中UML到Z的映射与转换机制。最后通过使用这个新的求精方法对一个实例求精来描述整个求精过程。     

Improving Generalization of Fuzzy IF--THEN Rules by Maximizing Fuzzy Entropy

When fuzzy IF--THEN rules initially extracted from data have not a satisfying performance, we consider that the rules require refinement. Distinct from most existing rule-refinement approaches that are based on the further reduction of training error, this paper proposes a new rule-refinement scheme that is based on the maximization of fuzzy entropy on the training set. The new scheme, which is realized by solving a quadratic programming problem, is expected to have the advantages of improving the generalization capability of initial fuzzy IF--THEN rules and simultaneously overcoming the overfitting of refinement. Experimental results on a number of selected databases demonstrate the expected improvement of generalization capability and the prevention of overfitting by a comparison of both training and testing accuracy before and after the refinement.      

Stepwise Development of Process-Algebraic Specifications in Decorated Trace Semantics

Process algebras are convenient formalisms to develop specifications stepwise. This can be done with the help of partially defined states in a specification. When refining the specification, new transitions are added to partially defined states. At every step, it is verified with the help of special preorders, refinement relations, that the step leads towards a desired goal. This approach has already been introduced in the case, where the verification is based on weak bisimulation equivalence. We show in this article that refinement relations can also be developed in decorated trace semantics. Moreover, the intuitive picture seems to be simpler in trace-based than in bisimulation-based semantics. The algorithms to compute the new refinement relations are exponential in the worst case, but behave quite well in practical cases.     

ART-2神经网络的改进及建模实现

指出了传统的ART-2神经网络对渐变过程不敏感的局限性,提出了一种新的改进算法。并对ART-2网络进行建模,通过与其它建模方法的对比,详尽讨论了ART-2的建模方法及特点。最后通过应用改进算法解决了原先模型中的“模式漂移”现象,使模型性能得到了明显的改善。     

Interpolatory √3-Subdivision

We present a new interpolatory subdivision scheme for triangle meshes. Instead of splitting each edge and performing a 1-to-4 split for every triangle we compute a new vertex for every triangle and retriangulate the old and the new vertices. Using this refinement operator the number of triangles only triples in each step. New vertices are computed with a Butterfly like scheme. In order to obtain overall smooth surfaces special rules are necessary in the neighborhood of extraordinary vertices. The scheme is suitable for adaptive refinement by using an easy forward strategy. No temporary triangles are produced here which allows simpler data structures and makes the scheme easy to implement.     

On the iterative refinement of the solution of ill-conditioned linear system of equations

Recently, Salkuyeh and Fahim [A new iterative refinement of the solution of ill-conditioned linear system of equations, Int. Comput. Math. 88(5) (2011), pp. 950–956] have proposed a two-step iterative refinement of the solution of an ill-conditioned linear system of equations. In this paper, we first present a generalized two-step iterative refinement procedure to solve ill-conditioned linear system of equations and study its convergence properties. Afterward, it is shown that the idea of an orthogonal projection technique together with a basic stationary iterative method can be utilized to construct a new efficient and neat hybrid algorithm for solving the mentioned problem. The convergence of the offered hybrid approach is also established. Numerical examples are examined to demonstrate the feasibility of proposed algorithms and their superiority to some of existing approaches for solving ill-conditioned linear system of equations.