The notion of SQL assertion was introduced, in SQL-92 standard, to define general constraints over a relational database. They can be used, for instance, to specify cross-row constraints or multitable check constraints. However, up to now, none of the current relational database management systems (RDBMSs) support SQL assertions due to the difficulty of providing an efficient solution. To implement SQL assertions efficiently, the RDBMs require an incremental checking mechanism. I.e., given an assertion, the RDBMS should revalidate it only when a transaction changes data in a manner that could violate it, and only for the affected data. Some years ago, the deductive database community provided several incremental checking methods, however, their results could not get into practice in RDBMS. In this paper, we propose an approach to efficiently implement SQL assertions in an RDBMS through an incremental revalidation technique. Such an approach is compatible with any RDBMS since it is fully based on standard SQL concepts (tables, triggers, and procedures). Our proposal uses and extends the Event Rules , an existing proposal for incremental checking in deductive databases. This extension is required to handle distributive aggregates, which pushes the expressiveness of the handled SQL assertions beyond first-order constraints. Moreover, we exploit this extension to improve the treatment of constraints involving existential variables, which are a very common kind of constraints difficult and expensive to handle. Finally, we show the efficiency of our approach through some experiments, and we formally prove its soundness and completeness.

One of the most difficult, time-consuming and error-prone tasks during software testing is that of manually generating the data required to properly run the test. This is even harder when we need to generate data of a certain size and such that it satisfies a set of conditions, or business rules, specified over an ontology. To solve this problem, some proposals exist to automatically generate database sample data. However, they are only able to generate data satisfying primary or foreign key constraints but not more complex business rules in the ontology. We propose here a more general solution for generating test data which is able to deal with expressive business rules. Our approach, which is entirely based on the chase algorithm, first generates a small sample of valid test data (by means of an automated reasoner), then clones this sample data, and finally, relates the cloned data with the original data. All the steps are performed iteratively until a valid database of a certain size is obtained. We theoretically prove the correctness of our approach, and experimentally show its practical applicability.

There are billions of devices worldwide deployed, connected, and communicating to other systems. Sensors and actuators, which can be stationary or movable devices. These Edge devices are considered part of the Internet of Things (IoT) devices, which can be referred to as a tier of the Computing Continuum paradigm. There are two main concerns at stake in the success of this ecosystem. The interoperability between devices and systems is the first. Mainly, because most of them communicate uniquely and differently from each other, leading to heterogeneous data. The second issue is the lack of decision-making capacity to conduct actuations, such as communicating through different computing tiers based on latency constraints due to a certain measured factor. In this article, we propose an ontology to improve device interoperability in the IoT. In addition, we also explain how to ease data communication between Computing Continuum devices, providing tools to enhance data management and decision-making. A use case is also presented, using the automotive industry, where quickness in maneuver determination is key to avoid accidents. It is exemplified using two Raspberry Pi devices, connected using different networks and choosing the appropriate one depending on context-aware conditions.

We present GROM, a tool conceived to handle high-level schema mappings between semantic descriptions of a source and a target database. GROM rewrites mappings between the virtual, view-based semantic schemas, in terms of mappings between the two physical databases, and then executes them. The system serves the purpose of teaching two main lessons. First, designing mappings among higher-level descriptions is often simpler than working with the original schemas. Second, as soon as the view-definition language becomes more expressive, to handle, for example, negation, the mapping problem becomes extremely challenging from the technical viewpoint, so that one needs to find a proper trade-off between expressiveness and scalability.

We present TINTIN, a tool to perform efficient integrity checking of SQL assertions in SQL Server. TINTIN rewrites each assertion into a set of standard SQL queries that, given a set of insertions and deletions of tuples, allow to incrementally compute whether this update violates the assertion or not. If one of such queries returns a non empty answer, then the assertion is violated. Efficiency is achieved by evaluating only those data and those assertions that can actually be violated according to the update. TINTIN is aimed at two different purposes. First, to show the feasibility of our approach by implementing it on a commercial relational DBMS. Second, to illustrate that the efficiency we achieve is good enough for making assertions to be used in practice.

Artifact-centric business process models have gained increasing momentum recently due to their ability to combine structural (i.e., data related) with dynamical (i.e., process related) aspects. In particular, two main lines of research have been pursued so far: one tailored to business artifact modeling languages and methodologies, the other focused on the foundations for their formal verification. In this paper, we merge these two lines of research, by showing how recent theoretical decidability results for verification can be fruitfully transferred to a concrete UML-based modeling methodology. In particular, we identify additional steps in the methodology that, in significant cases, guarantee the possibility of verifying the resulting models against rich first-order temporal properties. Notably, our results can be seamlessly transferred to different languages for the specification of the artifact lifecycles.

We describe a software architecture we have developed for a constructive containment checker of Entity SQL queries defined over extended ER schemas expressed in Microsoft's Entity Data Model. Our application of interest is compilation of object-to-relational mappings for Microsoft's ADO.NET Entity Framework, which has been shipping since 2007. The supported language includes several features which have been individually addressed in the past but, to the best of our knowledge, they have not been addressed all at once before. Moreover, when embarking on an implementation, we found no guidance in the literature on how to modularize the software or apply published algorithms to a commercially-supported language. This paper reports on our experience in addressing these real-world challenges.

To ensure the quality of an information system, it is essential that the conceptual schema that represents the knowledge about its domain is semantically correct. The semantic correctness of a conceptual schema can be seen from two different perspectives. On the one hand, from the point of view of its definition, a conceptual schema must be right . This is ensured by means of verification techniques that check whether the schema satisfies several correctness properties. On the other hand, from the point of view of the requirements that the information system should satisfy, a schema must also be the right one . This is ensured by means of validation techniques, which help the designer understand the exact meaning of a schema and to see whether it corresponds to the requirements. In this article we propose an approach to verify and validate UML conceptual schemas, with arbitrary constraints formalized in OCL. We have also implemented our approach to show its feasibility.

Schema mappings define relationships between schemas in a declarative way. We demonstrate MVT, a mapping validation tool that allows the designer to ask whether the mapping has certain desirable properties. The answers to these questions will provide information on whether the mapping adequately matches the intended needs and requirements. MVT is able to deal with a highly expressive class of mappings and database schemas, which allows the use of negations, order comparisons and null values. The tool does not only provide a Boolean answer as test result, but also a feedback for that result. Depending on the tested property and on the test result, the provided feedback can be in the form of example schema instances, or in the form of an explanation, that is, highlighting the mapping assertions and schema constraints responsible for getting such a result.

A query is unlively if it always returns an empty answer. Debugging a database schema requires not only determining unlively queries, but also fixing them. To the best of our knowledge, the existing methods do not provide the designer with an explanation of why a query is not lively. In this paper, we propose a method for computing explanations that is independent of the particular method used to determine liveliness. It provides three levels of search: one explanation, a maximal set of non-overlapping explanations, and all explanations. The first two levels require only a linear number of calls to the underlying method. We also propose a filter to reduce the number of these calls, and experimentally compare our method with the best known method for finding unsatisfiable subsets of constraints.

We show that database schema validation and update processing problems such as view updating, materialized view maintenance, integrity constraint checking, integrity constraint maintenance or condition monitoring can be classified as problems of either abductive or deductive nature, according to the reasoning paradigm that inherently suites them. This is done by performing abductive and deductive reasoning on the event rules (Olivé 1991), a set of rules that define the difference between consecutive database states. In this way, we show that it is possible to provide methods able to deal with all these problems as a whole. We also show how some existing general deductive and abductive procedures may be used to reason on the event rules. In this way, we show that these procedures can deal with all database schema validation and update processing problems considered in this paper.

We propose two interpretations of the event rules which provide a common framework for classifying and specifying deductive database updating problems such as view updating, materialized view maintenance, integrity constraints checking, integrity constraints maintenance, repairing inconsistent databases, integrity constraints satisfiability or condition monitoring. Moreover, these interpretations allow us to identify and to specify some problems that have received little attention up to now like enforcing or preventing condition activation. By considering only a unique set of rules for specifying all these problems, we want to show that it is possible to provide general methods able to deal with all these problems as a whole.>