17738680
Hierarchical Automata as Model for Statecharts
Statecharts are a very rich graphical specification formalism supported by the commercial tool Statemate. Statecharts comprises powerful concepts such as interlevel transitions, multiple-source/multiple-target transitions, priority amongst transitions and simultaneous execution of maximal non-conflicting sets of transitions. Every add-on tool which is supposed to be linked with the Statemate tool have to deal with the rather involved semantics of these concepts. We propose extended hierarchical automata as an intermediate format to facilitate the linking of new tools to the Statemate environment, whose main idea is to devise a simple formalism with a more restricted syntax than statecharts which nevertheless allows to capture the richer formalism. We define the format, give operational semantics to it, and translate statecharts to it.
33236770
Formal Verification of Stabilizing Systems
This paper links too formerly rather disjoint areas: formal verification and stabilization. Stabilization is a vitally emerging paradigm in fault tolerant distributed computing; formal verification investigates mathematically rigorous techniques to reason about systems.
209098159
The Code Validation Tool CVT: Automatic Verification of a Compilation Process.
62729675
The Composite Information System Laboratory (CISL) Project at MIT
The Composite Information Systems Laboratory (CISL) at MIT is involved in research on the strategic, organizational and technical aspects of the integration of multiple heterogeneous database systems. In this paper we examine the scope of the work being done at CISL. Certain research efforts in the technical areas of system integration are emphasized; in particular semantic aspects of the integration process and methods for tracking data sources in composite information systems.
7986917
Translation Validation: From DC+ to C*
Translation validation is an alternative to the verification of translators (compilers, code generators). Rather than proving in advance that the compiler always produces a target code which correctly implements the source code (compiler verification), each individual translation (i.e. a run of the compiler) is followed by a validation phase which verifies that the target code produced on this run correctly implements the submitted source program. In order to be a practical alternative to compiler verification, a key feature of this validation is its full automation. 
 
In this paper we demonstrate the feasibility of translation validation for industrial code generators from DC+ -a widely used intermediate format for synchronous languages- to C. We explain the compilation pattern from DC+ to C and advocate new abstraction techniques for a fragment of first order logic as part of the automation of our approach.
5683523
A Metadata Approach to Resolving Semantic Conflicts
In this paper we describe a rule-based approach to semantic specification that can be used to establish semantic agreement between a source and receiver. Query processing techniques use these specifications along with conversion routines and query modification to guarantee correct data semantics. This work also examines the effect of changing data semantics. These changes may occur at the source of the data or they may be changes in the specifications of the dat,a semantics for the application, Methods are described for detecting these changes and for determining if the database can continue to supply meaningful data to the application. These methods for semanlic reconcilia2ion are necessary for determining logical connectivity between a data source (database) and a data receiver (application). Though described in terms of the source-receiver model, these techniques can also be used for semantic reconciliation and schema integration for multidatabase systems. Keywords[data dictionaries, heterogeneous databases, metadata, query modification, schema integration, semantic conflicts]
16796441
Information integration with attribution support for corporate profiles
The proliferation of electronically available data within large organizations as well as publicly available data (e.g. over the World Wide Web) poses challenges for users who wish to efficiently interact with and integrate multiple heterogeneous sources. This paper presents CI3, a corporate information integrator, which applies XML as a tool to facilitate data mediation and integration amongst heterogeneous sources in the context of financial analysts creating corporate profiles. Sources include Lotus Notes, relational databases, and the World Wide Web. CI3 applies a unified XML data model to automate integration. By preserving metadata about the source of each datum in the integrated result set, CI3 supports source attribution. Users may trace the attribution metadata from the result back to the underlying sources and leverage their expertise in interpreting the data and, if necessary, use their judgment in assessing the authenticity and veracity of results. We present a functional overview of CI3, its system architecture including the XML data model, and the integration procedures. We conclude by reflecting on lessons learned.