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.     

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

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

Upgrading a Granular Computing Based Data Mining Framework to a Relational Case

One of the popular methods to develop an algorithm for mining data stored in a relational structure is to upgrade an existing attribute‐value algorithm to a relational case. Current approaches to this problem have some shortcomings such as (1) a dependence on the upgrading process of the algorithm to be extended, (2) complicated redefinitions of crucial notions (e.g., pattern generality, pattern refinement), and (3) a tolerant limitation of the search space for pattern discovery. In this paper, we propose and evaluate a general methodology for upgrading a data mining framework to a relational case. This methodology is defined in a granular computing environment. Thanks to our relational extension of a granular computing based data mining framework, the three above problems can be overcome.     

A relational approach to querying data streams

Data streams are long, relatively unstructured sequences of characters that contain information such as electronic mail or a tape backup of various documents and reports created in an office. A conceptual framework is presented, using relational algebra and relational databases, within which data streams may be queried. As information is extracted from the data streams, it is put into a relational database that may be queried in the usual manner. The database schema evolves as the user's knowledge of the content of the data stream changes. Operators are defined in terms of relational algebra that can be used to extract data from a specially defined relation that contains all or part of the data stream. This approach to querying data streams permits the integration of unstructured data with structured data. The operators defined extend the functionality of relational algebra in much the same way that the join does relative to the basic operators select, project, union, difference, and Cartesian product     

On the identification of verbs in computer programs of physiological models

The rationale for identifying verbs (actions modeled) in the source code of a mathematical model is presented, with algorithms leading to computational techniques for devising explanations of such models. Using flow graph methodology the source code of a program can be described as disjoint intervals of its directed acyclic graph. Intervals of this set containing complete loops represent the code structure conceptually equivalent to verbs modeled. In turn, such structures can be mapped uniquely as functional dependencies of the intensional form of a relational data base which is the model output. Simulation, then, can be viewed as retrieval, and the logical inferences of a model appear to be derivable via relational algebra of the data base. In these terms, a verb is a relation consisting of at least one variable defined in an interval. The relation's key attributes must include at least one variable, also defined in the interval. Verb definitions are essential if programs are to explain themselves.     

EXTENSION OF THE RELATIONAL DATABASE AND ITS ALGEBRA WITH ROUGH SET TECHNIQUES

This paper describes a database model based on the original rough sets theory. Its rough relations permit the representation of a rough set of tuples not definable in terms of the elementary classes, except through use of lower and upper approximations. The rough relational database model also incorporates indiscernibility in the representation and in all the operators of the rough relational algebra. This indiscernibility is based strictly on equivalence classes which must be defined for every attribute domain. There are several obvious applications for which the rough relational database model can more accurately model an enterprise than does the standard relational model. These include systems involving ambiguous, imprecise, or uncertain data. Retrieval over mismatched domains caused by the merging of one or more applications can be facilitated by the use of indiscernibility, and naive system users can achieve greater recall with the rough relational database. In addition, applications inherently “rough” could be more easily implemented and maintained in the rough relational database.     

RASES: A database supported framework for structured model base management

Structured management of model base has placed demands on some kind of computer based frameworks with highly structured formalisms. This paper proposes a new framework, called the relational algebraic system entity structure (RASES), which is based on the system entity structure (SES) formalism and the relational algebra (RA) formalism. These formalisms provide a conceptual basis for the structured model base management. Within the framework, structural knowledge of a system is represented in a hierarchical structure and saved in a database. Furthermore, several operations can be formulated in terms of relational algebra which can be coded in a standard query language such as the SQL. The framework can be easily implemented on, and fully utilize the functionality of, relational database management system (RDBMS). With the help of the implemented framework, simulation models can be systematically synthesized from the models in the model base through the following processes. First, a family of hierarchical structures of a system is organized in the form of entity structure by the entity structuring process. Then, candidate models of the system which meet design objectives are synthesized from the entity structure through the pruning process. Finally, designers can conduct appropriate experiment with the models for design verification and performance measure.     

A case study in mapping conceptual designs to object‐relational schemas

The recent emergence of object‐relational technology into the commercial database market has caused new challenges for the implementation of conceptual database designs. This paper presents our experience with using the Oracle 8 object‐relational data model in the implementation of an engineering application described using the EXPRESS conceptual modeling language. EXPRESS is part of the engineering community's Standard for the Exchange of Product Data and can be characterized as a structurally object‐oriented modeling language, supporting the notion of entities, entity hierarchies, complex constraints on entity hierarchies, relationships and inverse relationships between entities, and user‐defined types. As a result, EXPRESS provides an excellent framework for studying the mapping of conceptual modeling concepts into an object‐relational model. In this paper, we describe the way in which the features of EXPRESS can be mapped into object‐relational features such as object tables, object references, and nested tables. We also describe the manner in which features such as member functions on object types, triggers, and stored procedures can be used to support the implementation of constraints associated with a conceptual schema. Although the mappings presented are specific to EXPRESS and Oracle 8, the mappings are generalizable to conceptual modeling languages and object‐relational models with similar features. Our work defines how traditional mapping concepts must be revised in order to make adequate use of the features now found in object‐relational models. As part of this paper, we also compare our mapping approach using Oracle 8 to mapping issues for the PostgreSQL object‐relational model and the Objectivity/DB object‐oriented data model. Copyright © 2000 John Wiley & Sons, Ltd.     

Granular computing for relational data classification

We propose a novel framework for generating classification rules from relational data. This is a specialized version of the general framework intended for mining relational data and is defined in granular computing theory. In the framework proposed in this paper we define a method for deriving information granules from relational data. Such granules are the basis for generating relational classification rules. In our approach we follow the granular computing idea of switching between different levels of granularity of the universe. Thanks to this a granule-based relational data representation can easily be replaced by another one and thereby adjusted to a given data mining task, e.g. classification. A generalized relational data representation, as defined in the framework, can be treated as the search space for generating rules. On account of this the size of the search space may significantly be limited. Furthermore, our framework, unlike others, unifies not only the way the data and rules to be derived are expressed and specified, but also partially the process of generating rules from the data. Namely, the rules can be directly obtained from the information granules or constructed based on them.     

Simulation of MPI applications with time‐independent traces

Analyzing and understanding the performance behavior of parallel applications on parallel computing platforms is a long‐standing concern in the High Performance Computing community. When the targeted platforms are not available, simulation is a reasonable approach to obtain objective performance indicators and explore various hypothetical scenarios. In the context of applications implemented with the Message Passing Interface, two simulation methods have been proposed, on‐line simulation and off‐line simulation, both with their own drawbacks and advantages. In this work, we present an off‐line simulation framework, that is, one that simulates the execution of an application based on event traces obtained from an actual execution. The main novelty of this work, when compared to previously proposed off‐line simulators, is that traces that drive the simulation can be acquired on large, distributed, heterogeneous, and non‐dedicated platforms. As a result, the scalability of trace acquisition is increased, which is achieved by enforcing that traces contain no time‐related information. Moreover, our framework is based on a state‐of‐the‐art scalable, fast, and validated simulation kernel. We introduce the notion of performing off‐line simulation from time‐independent traces, propose and evaluate several trace acquisition strategies, describe our simulation framework, and assess its quality in terms of trace acquisition scalability, simulation accuracy, and simulation time. Copyright © 2014 John Wiley & Sons, Ltd.     

A novel framework for physically based sculpting and animation of free-form solids

This paper presents a new, physically based model for performing finite element simulation of deformable objects in which all quantities – strain, stress, displacement, etc. – are computed entirely in local frames of reference. In our framework, subdivision solids with non-homogeneous material properties, such as mass and deformation distributions, can be defined throughout continuous, volumetric domains. This capability enables an animator or virtual sculptor to exert fine-level control over deforming objects and to define a wide variety of physical behaviors. Furthermore, since all quantities pertinent to physical simulation are computed locally, our model facilitates both large-scale and small-scale deformations, as well as rigid or near-rigid transformations. We demonstrate applications of our framework in animation and interactive sculpting and show that interactive simulation of non-trivial, volumetric shapes is possible with our methodologies.     

Integration of object-oriented programming languages and database systems in KOPERNIK

KOPERNIK is an object-oriented database system, that allows uniform specification of database requests and application programs. The user interface is based on Smalltalk, and the object-oriented data model is represented in terms of classes and messages. Techniques are discussed for implementing such a model on top of an underlying relational database system. Those parts of application programs that cannot be translated into a relational language are handled by a Smalltalk processor. The semantics of the database requests is defined in terms of a meta-model and meta-messages, using an object-oriented approach. Hence we derive rules for translation of database requests into SQL queries over a binary relational view, introduced as an intermediate level between the underlying database and our conceptual view.     

CSP is a retract of CCS

Automata theory provides two ways of defining an automaton: either by its transition system, defining its states and events, or by its language, the set of sequences (traces) of events in which it can engage. For many classes of automaton, these forms of definition have been proved equivalent. For example, there is a well-known isomorphism between regular languages and finite deterministic automata. This paper suggests that for (demonically) the non-deterministic automata (as treated in process algebra), the appropriate link between transition systems and languages may be a retraction rather than an isomorphism.A pair of automata, defined in the tradition of CCS by their transition systems, may be compared by a pre-ordering based on some kind of simulation or bisimulation, for example, weak, strong, or barbed. Automata defined in the tradition of CSP are naturally ordered by set inclusion of their languages (often called refinement); variations in ordering arise from different choices of basic event, including for example, refusals and divergences. In both cases, we characterise a theory by its underlying transition system and its choice of ordering. Our treatment is therefore wholly semantic, independent of the syntax and definition of operators of the calculus.We put forward a series of retractions relating the above-mentioned versions of CSP to their corresponding CCS transition models. A retraction is an injection that is (with respect to the chosen ordering) monotonic, increasing and idempotent (up to equivalence). It maps the nodes of a transition system of its source theory to those of a system that has been saturated by additional transitions. Each retraction will be defined by a transition rule, in the style of operational semantics; the proofs use the familiar technique of co-induction, often abbreviated by encoding in the relational calculus.The aim of this paper is to contribute to unification of theories of reactive system programming. More practical benefits may follow. For example, we justify a method to improve the efficiency of model checking based on simulation. Furthermore, we show how model checking of a transition network fits consistently with theorem-proving tools, which reason directly about specifications and designs that are expressed in terms of sets of sequences of observable events.     

Inter-modelling with patterns

Inter-modelling is the activity of modelling relations between two or more modelling languages. The result of this activity is a model that describes the way in which model instances of these languages can be related. Many tasks in model-driven development can be classified as inter-modelling, for example designing model-to-model transformations, defining model matching and traceability relations, specifying model merging and model weaving, as well as describing mechanisms for inter-model consistency management and model synchronization. This paper presents our approach to inter-modelling in a declarative, relational, visual, and formal style. The approach relies on declarative patterns describing allowed or forbidden relations between two modelling languages. Such specification is then compiled into different operational mechanisms that are tailor-made for concrete inter-modelling scenarios. Up to now, we have used the approach to generate forward and backward transformations from a pattern specification. In this paper we demonstrate that the same specification can be used to derive mechanisms for other inter-modelling tasks, such as model matching and model traceability. In these scenarios the goals are generating the traces between two existing models, checking whether two models are correctly traced, and modifying the traces between two models if they are incorrect.     

Sound and mechanised compositional verification of input‐output conformance

This paper mechanises conformance verification in the setting of the CSP process algebra. The verification strategy is captured by a theorem stated as a process refinement expression, which can be verified by a model checker such as FDR. The conformance relation, cspio , distinguishes input and output events. The process algebraic framework of CSP is used to address compositional conformance verification by establishing compositionality properties for cspio with respect to the CSP operators. Although cspio has been defined in the standard CSP traces model, one can address quiescence situations using a special output event, in which case it is formally established that cspio is equivalent to Tretmans ioco . All the results have been mechanically proved using the CSP‐Prover. The proposed testing theory has been adopted in an industrial context involving collaboration with Motorola, on testing mobile applications. Several examples and a case study are presented to illustrate the overall approach. Copyright © 2013 John Wiley & Sons, Ltd.     

Querying fuzzy relational databases through fuzzy domain calculus

In this paper we present a definition of a domain relational calculus for fuzzy relational databases using the GEFRED model as a starting point. It is possible to define an equivalent fuzzy tuple relational calculus and consequently we achieve the two query language levels that Codd designed for relational databases but these are extended to fuzzy relational databases: Fuzzy relational algebra (defined in the GEFRED model) and the fuzzy relational calculus which is put forward in this paper. The expressive power of this fuzzy relational calculus is demonstrated through the use of a method to translate any algebraic expression into an equivalent expression in fuzzy domain relational calculus. Furthermore, we include a useful system so that the degree to which each value has satisfied the query condition can be measured. Some examples are also included in order to clarify the definition. ©1999 John Wiley & Sons, Inc.     

Petri nets modeling and analysis using extended bag-theoreticrelational algebra

Petri nets are a powerful modeling tool for studying reactive, concurrent systems. Analysis of the nets can reveal important information concerning the behavior of a modeled system. While various means for the analysis of the nets has been developed, a major limitation in the analysis, is explosion of large states space in simulation. An efficient method to manage large states space would overcome such a limitation. This paper proposes a framework for the modeling and analysis of Petri nets using relational database technologies. Formalism of the framework is based on a bag-theoretic relational algebra extended from the conventional, Within the framework, Petri nets are formalized by bag relations, and analysis algorithms are developed based on such formal relations. Properties associated with the nets are formalized by queries described in terms of the bag-theoretic relational algebra. The framework has been realized in a commercial relational database system using a standard SQL.