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.     

Relational Concurrent Refinement

Refinement in a concurrent context, as typified by a process algebra, takes a number of different forms depending on what is considered observable. Observations record, for example, which events a system is prepared to accept or refuse. Concurrent refinement relations include trace refinement, failures–divergences refinement, readiness refinement and bisimulation. Refinement in a state-based language such as Z, on the other hand, is defined using a relational model in terms of the input–output behaviour of abstract programs. These refinements are normally verified by using two simulation rules which help make the verification tractable. This paper unifies these two standpoints by generalising the standard relational model to include additional observable aspects. These are chosen in such a way that they represent exactly the notions of observation embedded in the various concurrent refinement relations. As a consequence, simulation rules for the tractable verification of concurrent refinement can be derived. We develop such simulation rules for failures–divergences refinement and readiness refinement in particular, using an alternative relational model in the latter case.     

Unifying Concurrent and Relational Refinement

Refinement in a concurrent context, as typified by a process algebra, takes a number of different forms depending on what is considered observable, where observations record, for example, which events a system is prepared to accept or refuse. Examples of concurrent refinement relations include trace refinement, failures-divergences refinement and bisimulation.Refinement in a state-based language such as Z, on the other hand, is defined using a relational model in terms of input/output behaviour of abstract programs. These refinements are verified by using two simulation rules which help make the verification tractable.The purpose of this paper is to unify these two standpoints, and we do so by generalising the standard relational model to include additional observable aspects. The central result of the paper is then to develop simulation rules to verify relations such as failures-divergences refinement in a relational setting, and show how these might be applied in a specification language such as Z.     

Relational concurrent refinement part III: traces,partial relations and automata

Data refinement in a state-based language such as Z is defined using a relational model in terms of the behaviour of abstract programs. Downward and upward simulation conditions form a sound and jointly complete methodology to verify relational data refinements, which can be checked on an event-by-event basis rather than per trace. In models of concurrency, refinement is often defined in terms of sets of observations, which can include the events a system is prepared to accept or refuse, or depend on explicit properties of states and transitions. By embedding such concurrent semantics into a relational framework, eventwise verification methods for such refinement relations can be derived. In this paper, we continue our program of deriving simulation conditions for process algebraic refinement by defining further embeddings into our relational model: traces, completed traces, failure traces and extension. We then extend our framework to include various notions of automata based refinement.     

Structural Refinement of Systems Specified in Object-Z and CSP

This paper is concerned with methods for refinement of specifications written using a combination of Object-Z and CSP. Such a combination has proved to be a suitable vehicle for specifying complex systems which involve state and behaviour, and several proposals exist for integrating these two languages. The basis of the integration in this paper is a semantics of Object-Z classes identical to CSP processes. This allows classes specified in Object-Z to be combined using CSP operators. It has been shown that this semantic model allows state-based refinement relations to be used on the Object-Z components in an integrated Object-Z/CSP specification. However, the current refinement methodology does not allow the structure of a specification to be changed in a refinement, whereas a full methodology would, for example, allow concurrency to be introduced during the development life-cycle. In this paper, we tackle these concerns and discuss refinements of specifications written using Object-Z and CSP where we change the structure of the specification when performing the refinement. In particular, we develop a set of structural simulation rules which allow single components to be refined to more complex specifications involving CSP operators. The soundness of these rules is verified against the common semantic model and they are illustrated via a number of examples.     

On the specification of modal systems: A comparison of three frameworks

This paper studies the relationships between three notions of behavioural preorder that have been proposed in the literature: refinement over modal transition systems, and the covariant–contravariant simulation and the partial bisimulation preorders over labelled transition systems. It is shown that there are mutual translations between modal transition systems and labelled transition systems that preserve, and reflect, refinement and the covariant–contravariant simulation preorder. The translations are also shown to preserve the modal properties that can be expressed in the logics that characterize those preorders. A translation from labelled transition systems modulo the partial bisimulation preorder into the same model modulo the covariant–contravariant simulation preorder is also offered, together with some evidence that the former model is less expressive than the latter. In order to gain more insight into the relationships between modal transition systems modulo refinement and labelled transition systems modulo the covariant–contravariant simulation preorder, their connections are also phrased and studied in the context of institutions.     

Using the Alloy Analyzer to Verify Data Refinement in Z

In the development of critical systems, standards dictate that it is necessary to first design, construct and formally analyse abstract models of the system. Developers must then verify that the final implementation is consistent with these more abstract specifications.Z is an example of a state-based specification language. It has been shown to be effective in a variety of cases—indeed it was developed as part of a joint collaboration between Oxford University's PRG and IBM Hursley for the specification of the CICS system. However, Z's main weakness is that it does not have the necessary tool support: whilst there are associated type checkers, there is no tool for automatically verifying refinement in Z.The contribution of this paper is to show how data refinement in Z can be automatically verified using the Alloy Analyzer. The soundness and joint completeness of the simulation rules for Z have already been established: here we translate them to Alloy. We then show how data types expressed in Z can also be translated to Alloy, before presenting the assertions necessary for the Alloy Analyzer to identify the retrieve relation and hence verify refinement. We present a simple example in which the Alloy Analyzer successfully identifies the retrieve relation between two data types thereby verifying simulation and hence refinement. We conclude the paper with a discussion of the suitability of the Alloy Analyzer for such a task.     

Simulation Guided Hair Dynamics Modeling from Video

In this paper we present a hybrid approach to reconstruct hair dynamics from multi‐view video sequences, captured under uncontrolled lighting conditions. The key of this method is a refinement approach that combines image‐based reconstruction techniques with physically based hair simulation. Given an initially reconstructed sequence of hair fiber models, we develop a hair dynamics refinement system using particle‐based simulation and incompressible fluid simulation. The system allows us to improve reconstructed hair fiber motions and complete missing fibers caused by occlusion or tracking failure. The refined space‐time hair dynamics are consistent with video inputs and can be also used to generate novel hair animations of different hair styles. We validate this method through various real hair examples.     

Calculating upward and downward simulations of state-based specifications

This paper concerns calculational methods of refinement in state-based specification languages. Data refinement is a well-established technique for transforming specifications of abstract data types into ones, which are closer to an eventual implementation. The conditions under which a transformation is a correct refinement are encapsulated into two simulation rules: downward and upward simulations.One approach for refining an abstract system is to specify the concrete data type, and then attempt to verify that it is a valid refinement of the abstract type. An alternative approach is to calculate the concrete specification based upon the abstract specification and a retrieve relation, which links the abstract and concrete states. In this paper we generalise existing calculational methods for downward simulations and derive similar results for upward simulations; we also document their use and application in a particular specification language, namely Z.     

Refinement is complete for implementations

Modal transition systems specify sets of implementations, their refining labelled transition systems, through Larsen & Thomsen’s co-inductive notion of refinement. We demonstrate that refinement precisely captures the identification of a modal transition system with its set of implementations: refinement is reverse containment of sets of implementations. This result extends to models that combine state and event observables and is drawn from a SFP-domain whose elements are equivalence classes of modal transition systems under refinement [HJS04], and abstraction-based finite-model properties proved in this paper. As a corollary, validity checking is model checking for Hennessy-Milner formulas that characterize modal transition systems with bounded computation paths. We finally sketch how techniques developed in this paper can be used to detect inconsistencies between multiple modal transition systems and, if consistent, to verify properties of all common implementations.Received January 2004Revised August 2004Accepted December 2004 by M. Leuschel and D. J. Cooke     

Blaming the client: on data refinement in the presence of pointers

Data refinement is a common approach to reasoning about programs, based on establishing that a concrete program indeed satisfies all the required properties imposed by an intended abstract pattern. Reasoning about programs in this setting becomes complex when use of pointers is assumed and, moreover, a well-known method for proving data refinement, namely the forward simulation method, becomes unsound in presence of pointers. The reason for unsoundness is the failure of the “lifting theorem” for simulations: that a simulation between abstract and concrete modules can be lifted to all client programs. The result is that simulation does not imply that a concrete can replace an abstract module in all contexts. Our diagnosis of this problem is that unsoundness is due to interference from the client programs. Rather than blame a module for the unsoundness of lifting simulations, our analysis places the blame on the client programs which cause the interference: when interference is not present, soundness is recovered. Technically, we present a novel instrumented semantics which is capable of detecting interference between a module and its client. With use of special simulation relations, namely growing relations, and interpreting the simulation method using the instrumented semantics, we obtain a lifting theorem. We then show situations under which simulation does indeed imply refinement.     

基于模拟关系的精化检测方法

精化检测是一种重要的形式化验证方法,将系统实现和性质规约用相同形式化语言进行建模,如能证明两者间存在某种精化关系且该关系能够维持性质,可得出系统实现满足性质规约.为验证不同类型的系统性质, traces、stable failures和failures-divergence精化检测方法已被提出.精化检测算法依赖于子集构造,因而其面临状态空间爆炸问题.近年来,已有学者针对NFA语言包含问题提出了基于模拟关系的状态空间消减方法,大大提高了算法性能,且该方法能直接用于traces精化检测.在此基础上,本文提出了基于模拟关系的stable failures和failures-divergence精化检测方法.此外,本文还将精化检测扩展到了时间系统的验证中,提出了基于模拟关系的时间自动机traces精化检测方法.实验结果表明,基于模拟关系的算法效率有很大提高.     

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.     

Real‐time cutting simulation of meshless deformable object using dynamic bounding volume hierarchy

This paper proposes a novel method for a real‐time cutting simulation of deformable objects using meshless method. The method utilizes a rapid refinement of topological relations among the simulation nodes of meshless deformable objects. Topological relations are defined as an undirected graph based on a visibility criterion. The graph connects the adjacent nodes that lie within a support of each node. The topological relations are refined by removing the edges of the graph that is intersected by the cut surface during the cutting simulation. Our approach utilizes a bounding volume hierarchy (BVH) to accelerate the computation of the intersection test. The BVH reconstruction algorithm is proposed to account for the cases where pieces of the object are completely cut out from the object. Algorithms to examine the connectivity among simulation nodes and accordingly reconstructing the BVH using two‐level BVH are presented. The proposed approach achieves real‐time cutting simulation of deformable objects through the rapid refinement of the topological relation. In addition, the computational performance of the cutting procedure is preserved during the entire simulation, thanks to the real‐time reconstruction of the BVH. Copyright © 2012 John Wiley & Sons, Ltd.     

Content reference: Reasoning about rules

In a companion paper [1] we described the concept of saturation, the situation in a program in which so many knowledge sources (KSs) are potentially useful at each invocation cycle that it is unrealistic to consider unguided, exhaustive invocation. We argued that saturation appears almost inevitable in large AI programs.We suggested that the process of invocation can be viewed as occurring in three steps: retrieval (selecting some subset of KSs from the knowledge base), refinement (pruning or reordering that subset), and execution (executing one or more of the KSs). We then argued that one useful approach to dealing with saturation is by embedding intelligence in the refinement phase, and described meta-rules, a means of encoding knowledge used to effect refinement.In this paper we consider a more detailed, ‘engineering’ issue, but one with a number of interesting implications: While there are many ways to implement refinement, we suggest that one particular technique—which we call content reference—offers a number of advantages, including giving the system some ability to reason about the content of its knowledge.     

一种基于构件演算的主动构件精化方法

现代构件系统通常包含多个并发执行的主动构件,这使得验证构件系统的正确性变得十分困难.通过对构件演算进行扩展,提出了一种主动构件的精化方法.在构件接口层引入契约.契约使用卫式设计描述公共方法和主动活动的功能规约.通过一对发散、失败集合定义契约的动态行为,并利用发散、失败集合之间的包含关系定义契约间的精化关系.证明了应用仿真技术确认契约精化关系的定理.定义构件的语义为其需求接口契约到其服务接口契约的函数,以此为基础,可以通过契约的精化来证明构件的精化.给出了构件的组装规则.在构件系统自底向上的构造过程中,应用构件的精化方法和组装规则可以保证最终系统的正确性.     

Verification of Mondex electronic purses with KIV: from transactions to a security protocol

The Mondex case study about the specification and refinement of an electronic purse as defined in the Oxford Technical Monograph PRG-126 has recently been proposed as a challenge for formal system-supported verification. In this paper we report on two results. First, on the successful verification of the full case study using the KIV specification and verification system. We demonstrate that even though the hand-made proofs were elaborated to an enormous level of detail we still could find small errors in the underlying data refinement theory, as well as the formal proofs of the case study. Second, the original Mondex case study verifies functional correctness assuming a suitable security protocol. We extend the case study here with a refinement to a suitable security protocol that uses symmetric cryptography to achieve the necessary properties of the security-relevant messages. The definition is based on a generic framework for defining such protocols based on abstract state machines (ASMs). We prove the refinement using a forward simulation. J. C. P. Woodcock     

Applications of stencil-adaptive finite difference method to incompressible viscous flows with curved boundary

This paper investigates the applicability of the stencil-adaptive finite difference method for the simulation of two-dimensional unsteady incompressible viscous flows with curved boundary. The adaptive stencil refinement algorithm has been proven to be able to continuously adapt the stencil resolution according to the gradient of flow parameter of interest [Ding H, Shu C. A stencil adaptive algorithm for finite difference solution of incompressible viscous flows. J Comput Phys 2006;214:397-420], which facilitates the saving of the computational efforts. On the other hand, the capability of the domain-free discretization technique in dealing with the curved boundary provides a great flexibility for the finite difference scheme on the Cartesian grid. Here, we show that their combination makes it possible to simulate the unsteady incompressible flow with curved boundary on a dynamically changed grid. The methods are validated by simulating steady and unsteady incompressible viscous flows over a stationary circular cylinder.     

Formal Verification Techniques Based on Boolean Satisfiability Problem

This paper exploits Boolean satisfiability problem in equivalence checking and model checking respectively. A combinational equivalence checking method based on incremental satisfiability is presented. This method chooses the candidate equivalent pairs with some new techniques, and uses incremental satisfiability algorithm to improve its performance.By substituting the internal equivalent pairs and converting the equivalence relations into conjunctive normal form (CNF)formulas, this approach can avoid the false negatives, and reduce the search space of SAT procedure. Experimental results on ISCAS‘85 benchmark circuits show that, the presented approach is faster and more robust than those existed in literature.This paper also presents an algorithm for extracting of unsatisfiable core, which has an important application in abstraction and refinement for model checking to alleviate the state space explosion bottleneck. The error of approximate extraction is analyzed by means of simulation. An analysis reveals that an interesting phenomenon occurs, with the increasing density of the formula, the average error of the extraction is decreasing. An exact extraction approach for MU subformula, referred to as pre-assignment algorithm, is proposed. Both theoretical analysis and experimental results show that it is more efficient.