Search

In this paper proposes a method for the generation of tests instances from business rules of a system, expressed using OCL. The aim of this method is to give one a better support for test activities like, for example, the generation of tests instances to test models in the initial phases of the software development lifecycle, showing the inconsistencies and ambiguities in earlier in the project. A differential of this method, compared to others with similar intention, is that, beyond the generation of the test cases, the generated tests could be validated and be followed in an automatized way through the USE tool. To help in the execution of the proposed method, the TestiMonium tool was implemented and integrated to the environment. [ABSTRACT FROM PUBLISHER]

Abstract: Background: The treatment of osteochondral lesions, especially those with a cystic component or those that have failed the standard arthroscopic procedures can be challenging. Synthetic grafts have several potential advantages over other second line treatments including the fact that only one operation is required and no other joint is violated. Method: We report the results of the first series of synthetic grafts used in the treatment of osteochondral lesions of the ankle with a minimum of one year follow up. Results: There was significant improvement in the American Orthopaedic Foot & Ankle Society (AOFAS) Hindfoot and Ankle Osteoarthritis Scale (AOS) scores and all patients were satisfied with the results of surgery. Magnetic Resonance Imaging (MRI) scans at one year have demonstrated resolution of the bony cysts and surrounding bone marrow oedema but, worryingly, continued to show high signal on the T2 weighted images within the plugs themselves. Qualitative T2 mapping has suggested a fibrous rather than hyaline appearance of the cartilage portions of the plugs. Conclusions: The clinical results have been encouraging but more patients and longer follow up are required before firm conclusions can be drawn. [Copyright &y& Elsevier]

Since several years, the Object Constraint Language (OCL) is a central component in modeling and transformation languages like the Unified Modeling Language, the Meta Object Facility, and Query View Transformation. Consequently, approaches MDE (Model-Driven Engineering) depend on this language. OCL is present not only in areas influenced by the OMG but also in the Eclipse Modeling Framework (EMF). Thus the quality of OCL and its realization in tools seems to be crucial for the success of model-driven development. Surprisingly, up to now a benchmark for OCL to measure quality properties has not been proposed. This paper puts forward in the first part the concepts of a comprehensive OCL benchmark. Our benchmark covers (1) OCL engine accuracy (e.g., for the handling of the undefined value, the use of variables and the implementation of OCL standard operations), (2) OCL engine determinateness properties (e.g., for the collection operations 'any' and 'flatten'), and (3) OCL engine efficiency (for data type and user-defined operations). In the second part, this paper empirically evaluates the proposed benchmark concepts by examining several OCL tools. The paper clarifies a number of differences in handling particular language features and under specifications in the OCL standard. [ABSTRACT FROM AUTHOR]

BPMN is becoming the de facto standard for process description, analysis and simulation, in IT and many other business domains. BPMN supports different levels of abstraction, from high-level process models, to detailed models capable of being executed. Several tools now support, at least partly, OMG's BPMN metamodel specification. However, while several other OMG's metamodels include a formal specification of well-formedness rules, using OCL, the BPMN metamodel specification only includes those rules in natural language, scattered across several hundred pages of that document. Not surprisingly, we found that all mainstream BPMN tools do not enforce those well-formedness rules, while checking the correctness of process models. Model preciseness enforcement is important to mitigate ambiguity. The latter hampers the achievement of a shared meaning among process stakeholders, is detrimental to process reuse and is unacceptable if we look for executable processes. To enforce model preciseness we propose to supplement the OMG BPMN metamodel with well-formedness rules expressed as OCL invariants. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

Au cours de ces dernières années, plusieurs approches ont abordé la modélisation et le développement des Entrepôts de Données (ED). La plupart de ces approches fournit des solutions partielles qui traitent soit la modélisation multidimensionnelle, soit la modélisation des processus d’Extraction-Transformation-Chargement. Toutefois, peu de travaux ont visé à unifier ces deux problématiques dans un cadre structuré ou à automatiser le processus d’entreposage complet. Afin de pallier ces limites, nous proposons dans ce papier une démarche unifiée et automatique qui intègre la modélisation des ED et des processus ETL. Cette démarche est définie dans le cadre d’une Architecture Dirigée par les Modèles (MDA). Elle permet (i) de formaliser les besoins des décideurs, ensuite (ii) de générer les modèles conceptuel, logique et physique de l’ED et des processus ETL conjoints (iii) ainsi que les codes de création et d’alimentation (ETL) des structures multidimensionnelles. Les règles de transformation entre modèles sont formalisées en Query/View/Transformation. During the last few years, several frameworks have dealt with Data Warehousing (DW) design issues. Most of these frameworks provide partial answers that focus either on multidimensional modelling (MD) or on Extraction-Transformation-Loading modelling (ETL). However, less attention has been given neither to unifying both modelling issues into a single structured framework nor to automating the warehousing process. To overcome these limits, this paper provides a generic unified and automated method that integrates DW and ETL processes design. The framework is handled within the Model Driven Architecture (MDA). It (i) first helps the designer in modelling the decision-maker’s requirements and then (ii) generates the MD model as well as (iii) the logical and the physical models and finally (iv) generates the code. In this approach, the transformation rules are formalized using the Query/View/Transformation (QVT) language. [ABSTRACT FROM PUBLISHER]

In this paper, we report on our current work toward efficient and effective verification of web application's basic design. We use a UML class diagram with Object Constraint Language (OCL) to describe the application behaviors and data constraints. Then we generate test data from the formally represented specifications. We make the observation that key web application behaviors can be captured through table size constraints as well as data constraints like foreign key constraints. Based on the observation, we translate the OCL specification into the equivalent constraints using table size expressions. We present a scheme to generate test data from the translated constraints using a Satisfiability Modulo Theories solver. We employ two techniques to reduce constraints. The first is string handling and the other is decomposition of table structures. We also report on an experimental result of test data generation. The result indicates a potential that our scheme works well for real applications in reasonable times. [ABSTRACT FROM AUTHOR]

The continuing evolution of business needs and technology makes Web applications more complex in terms of development, maintenance, and management. To cope with this complexity, several Frameworks have emerged. Given this diversity of solutions, the generation of a code based on UML models has become a necessity. This paper presents the application of the MDA (Model Driven Architecture) to generate, from the UML model, the Code following the MVC2 pattern (Model-View-Controller) using the standard MOF 2.0 QVT (Meta-Object Facility Model 2.0 Query-View-Transformation) as a transformation language. This standard defines the meta-model for the development of model transformation. The transformation rules defined in this paper can generate, from the class diagram, an XML file containing the Actions, the Forms, and JSP pages. This file can be used to generate the necessary code of a web application. [ABSTRACT FROM AUTHOR]

Copyright of Enl@ce: Revista Venezolana de Información, Tecnología y Conocimiento is the property of Universidad del Zulia, Laboratorio de Investigacion y Sistemas de Informacion and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)

In agricultural research, to carry out experimental ex post evaluations, it is first necessary to design and evaluate a high number of Cropping Systems (CS). CRITER has recently been proposed as a tool to evaluate a priori these CS, spatially at the farm level and temporally at the crop succession level. In relation to the development of software applications in general and more particularly in the field of agronomic research, the most innovative aspect of our work is our Model-Driven Development approach. To construct CRITER we have adopted the Model-Driven Architecture (MDA) of the Object Management Group (OMG) which is based on the Meta-Object Facility (MOF) language. We have used the Enterprise Core Object (ECO) framework of the DELPHI Integrated Development Environment (IDE). The ECO framework helps the modeler at different steps of software development, from the graphical design in UML to the automatic code generation. The result is a fully navigable class diagram which allows us: (1) to build, in a simple way with few OCL expressions, the user interfaces; (2) to integrate commercial and user data bases via the automatic mapping of a class model to a relational data base schema; and (3) to easily implement the computation of the different indicators. Modelers can therefore focus on their business model rather than on the technical aspects of programming. [ABSTRACT FROM AUTHOR]

A core challenge in biomedical data integration is to enable semantic interoperability between its various stakeholders as well as other interested parties. Promoting the adoption of worldwide accepted information standards along with common controlled terminologies is the right path to achieve this. Our paper describes a solution to this fundamental problem by proposing an approach to semantic data integration based on information models serving as a common language to represent health data coupled with technology that is able to represent the data semantics. We used the HL7 v3 Reference Information Model (RIM) [1] to derive a specific data model for the integrated data, the Web Ontology Language (OWL) [2] to build an ontology that harmonizes the metadata from the disparate data sources, the Unified Modeling Language (UML) [3] to model the data representation, and the Object Constraint Language (OCL) [4] to specify UML model constraints. To illustrate the approach, we use the Essential Hypertension Summary CDA document and related models from Hypergenes, a European Commission funded project [5] exploring the Essential Hypertension disease model. [ABSTRACT FROM AUTHOR]

A number of coverage criteria have been proposed for testing classes and class clusters modeled with state machines. Previous research has revealed their limitations in terms of their capability to detect faults. As these criteria can be considered to execute the control flow structure of the state machine, we are investigating how data flow information can be used to improve them in the context of UML state machines. More specifically, we investigate how such data flow analysis can be used to further refine the selection of a cost-effective test suite among alternative, adequate test suites for a given state machine criterion. This paper presents a comprehensive methodology to perform data flow analysis of UML state machines—with a specific focus on identifying the data flow from OCL guard conditions and operation contracts—and applies it to a widely referenced coverage criterion, the round-trip path (transition tree) criterion. It reports on two case studies whose results show that data flow information can be used to select the best transition tree, in terms of cost effectiveness, when more than one satisfies the transition tree criterion. The results also suggest that different trees are complementary in terms of the data flow that they exercise, thus, leading to the detection of intersecting but distinct subsets of faults. Copyright © 2009 John Wiley & Sons, Ltd. [ABSTRACT FROM AUTHOR]

In this paper we present an approach for the analysis of graph transformation rules based on an intermediate OCL representation. We translate different rule semantics into OCL, together with the properties of interest (like rule applicability, conflicts or independence). The intermediate representation serves three purposes: (1) it allows the seamless integration of graph transformation rules with the MOF and OCL standards, and enables taking the meta-model and its OCL constraints (i.e. well-formedness rules) into account when verifying the correctness of the rules; (2) it permits the interoperability of graph transformation concepts with a number of standards-based model-driven development tools; and (3) it makes available a plethora of OCL tools to actually perform the rule analysis. This approach is especially useful to analyse the operational semantics of Domain Specific Visual Languages. We have automated these ideas by providing designers with tools for the graphical specification and analysis of graph transformation rules, including a back-annotation mechanism that presents the analysis results in terms of the original language notation. [ABSTRACT FROM AUTHOR]

Abstract: UML is currently the most widely used modeling language for the specification of the conceptual schema (CS) of an information system (IS). However, UML falls short when it comes to allow business people to define in their own language (e.g. using their own terms in natural language) the policies and rules by which they run their business. To this purpose, the semantics of business vocabulary and business rules (SBVR) metamodel specification was proposed. SBVR is conceptualized optimally for business people and it is designed to be used for business purposes, independently of information systems designs. Clearly, SBVR and unified modeling language (UML) cannot be considered as isolated languages. Many of the business rules specified by business people must be automatically executed by the underlying information system, and thus, they must also appear in its UML CS. In this sense, the main goal of this paper is to bridge the gap between UML and SBVR by providing an automatic transformation from UML to SBVR specifications. Thanks to our transformation, designers will be able to interact with the business people (in their own language) to refine and validate the information modeled in the CS before the generation of the final IS implementation. Our transformation also takes into account all possible textual object constraint language (OCL) expressions that complement the UML graphical elements. [Copyright &y& Elsevier]

Use case (UC) modeling is a popular requirements modeling technique. While these models are simple to create and read; this simplicity is often misconceived, leading practitioners to believe that creating high quality models is straightforward. Therefore, many low quality models that are inconsistent, incorrect, contain premature restrictive design decision and contain ambiguous information are produced. To combat this problem of creating low quality UC models, this paper presents a new technique that utilizes antipatterns as a mechanism for remedying quality problems in UC models. The technique, supported by the tool ARBIUM, provides a framework for developers to define antipatterns. The feasibility of the approach is demonstrated by applying it to a real-world system. The results indicate that applying the technique improves the overall quality and clarity of UC models. [ABSTRACT FROM AUTHOR]

Precision and consistency are important prerequisites for class models to conform to their intended domain semantics. Precision can be achieved by augmenting models with design constraints and consistency can be achieved by avoiding contradictory constraints. However, there are different views of what constitutes a contradiction for design constraints. Moreover, state-of-the-art analysis approaches for proving constrained models consistent either scale poorly or require the use of interactive theorem proving. In this paper, we present a heuristic approach for efficiently analyzing constraint specifications built from constraint patterns. This analysis is based on precise notions of consistency for constrained class models and exploits the semantic properties of constraint patterns, thereby enabling syntax-based consistency checking in polynomial-time. We introduce a consistency checker implementing these ideas and we report on case studies in applying our approach to analyze industrial-scale models. These studies show that pattern-based constraint development supports the creation of concise specifications and provides immediate feedback on model consistency. [ABSTRACT FROM AUTHOR]

The specification of a software system must include all relevant static and dynamic aspects of the domain. Dynamic aspects are usually specified by means of a behavioral schema consisting of a set of system operations that the user may execute to update the system state. To be useful, such a set must be complete (i.e. through these operations, users should be able to modify the population of all elements in the class diagram) and executable (i.e. for each operation, there must exist a system state over which the operation can be successfully applied). A manual specification of these operations is an error-prone and time-consuming activity. Therefore, the aim of this paper is to present a strategy for the automatic generation of a basic behavior schema. Operations in the schema are drawn from the static aspects of the domain as defined in the UML class diagram and take into account possible dependencies among them to ensure the completeness and executability of the operations. We believe our approach is especially useful in a Model-Driven Development setting, where the full implementation of the system is derived from its specification. In this context, our approach facilitates the definition of the behavioral specification and ensures its quality obtaining, as a result, an improved code generation phase. [ABSTRACT FROM AUTHOR]

The article presents a study on the use of model transformations to bridge the abstract and concrete syntax of Web rule languages. Web rule languages, including the Semantic Web Rule Language (SWRL), Rule Markup Language (R2ML) and Object Constraint Language (OCL), are used to define the abstract and concrete syntax separately. Model driven engineering (MDE) can be used in identifying the type of reasoning to be used in semantic Web research. Details on the research implementation are included.

Copyright of Enl@ce: Revista Venezolana de Información, Tecnología y Conocimiento is the property of Universidad del Zulia, Laboratorio de Investigacion y Sistemas de Informacion and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)

Business rules are important components of every business system. Therefore creating information systems aimed to support business it is important to specify business rules unambiguously. Formal specification languages have different power specifying business rules of different types. This work argues that formal language OCL powerful enough to specify business rules of main types.

Contracts provide a precise way of specifying object-oriented systems. When a class structure is modified, the corresponding contracts must be modified accordingly. This paper presents a method of transforming contracts, which allows the extension of a mapping defined on a few model elements, to—what we call—an interpretation function, and to use this function to automatically translate OCL-constraints. Interestingly, such functions preserve reasoning using propositional calculi, resolution, equations, and induction. Interpretation functions can be used to trace model elements throughout multiple redesigns of UML class diagrams in both the forward, and the backward direction. The applicability of our approach is demonstrated in several examples, including some of Fowler’s refactoring patterns. [ABSTRACT FROM AUTHOR]

Due to their complexity, the syntax of modern modeling languages is preferably defined in two steps. The abstract syntax identifies all modeling concepts whereas the concrete syntax should clarify how these concepts are rendered by graphical and/or textual elements. While the abstract syntax is often defined in form of a metamodel, there does not exist such standard format yet for concrete syntax definitions. The diversity of definition formats—ranging from EBNF grammars to informal text—is becoming a major obstacle for advances in modeling language engineering, including the automatic generation of editors. In this paper, we propose a uniform format for concrete syntax definitions. Our approach captures both textual and graphical model representations and even allows to assign more than one rendering to the same modeling concept. Consequently, following our approach, a model can have multiple, fully equivalent representations, but—in order to avoid ambiguities when reading a model representation—two different models should always have distinguishable representations. We call a syntax definition correct, if all well-formed models are represented in a non-ambiguous way. As the main contribution of this paper, we present a rigorous analysis technique to check the correctness of concrete syntax definitions. [ABSTRACT FROM AUTHOR]

Prototyping is an efficient and effective way to understand and validate system requirements at the early stage of software development. In this paper, we present an approach for transforming UML system requirement models with OCL specifications into executable prototypes with the function of checking multiplicity and invariant constraints. Generally, a use case in UML can be described as a sequence of system operations. A system operation can be formally defined by a pair of preconditions and postconditions specified using OCL in the context of the conceptual class model. By analyzing the semantics of the preconditions and postconditions, the execution of the operation can be prototyped as a sequence of primitive actions which first check the precondition, and then enforce the postcondition by transferring the system from a pre-state to a post-state step by step. The primitive actions are basic manipulations of the system state (an object diagram), including find objects and links, create and remove objects and links, and check and set attribute values. Based on this approach, we have developed a tool of automatic prototype generation and analysis: AutoPA3.0. [ABSTRACT FROM AUTHOR]

In a software lifetime, during definition and analysis stages, a specification of requirements is carried out. For such a purpose, it is necessary to get through a process to capture interested persons' needs and expectations, which will later be translated into a set of models representing both the problem and the solution. Most models are frequently expressed by the UML (Unified Modeling Language) which defines a set of devices for specifying software requirements which should be consistent with the same model. However, consistency among several devices is not defined in the UML specification and not too much work has been made with this type of consistence. This article proposes a method to verify consistence among UML class diagram and use case diagram in a formal way. Such a process is carried out through an evaluation of several rules defined in the OCL (Object Constraint Language), which should be fulfilled to assure that information provided by such models is consistent. As both diagrams participation is recognized when preparing GUI (Graphic User Interfaces) consistence with this device is additionally defined [ABSTRACT FROM AUTHOR]

UML currently still lacks a rigorously defined semantics for its models, which makes formally analyzing a model and verifying its properties extremely difficult. To remedy that, we first present a technique for transforming the UML statechart diagrams into Petri nets. Then we develop an approach based on the class association ends. This approach shows how to validate the system invariants, expressed in the Object Constraint Language, on the Petri nets derived from the UML models. System property validation starts with an initialization of the model, extracted from the object and sequence diagrams. A case study is given throughout the paper to illustrate the methodology. [ABSTRACT FROM AUTHOR]

Abstract: The Unified Modeling Language (UML) is accepted today as an important standard for developing software. UML tools however provide little support for validating and checking models in early development phases. There is also no substantial support for the Object Constraint Language (OCL). We present an approach for the validation of UML models and OCL constraints based on animation and certification. The USE tool (UML-based Specification Environment) supports analysts, designers and developers in executing UML models and checking OCL constraints and thus enables them to employ model-driven techniques for software production. [Copyright &y& Elsevier]

Constraints play a key role in the definition of conceptual schemas. In the UML, constraints are usually specified by means of invariants written in the OCL. However, due to the high expressiveness of the OCL, the designer has different syntactic alternatives to express each constraint. The techniques presented in this paper assist the designer during the definition of the constraints by means of generating equivalent alternatives for the initially defined ones. Moreover, in the context of the MDA, transformations between these different alternatives are required as part of the PIM-to-PIM, PIM-to-PSM or PIM-to-code transformations of the original conceptual schema. [Copyright &y& Elsevier]

The Object Constraint Language (OCL) is a subset of the well-known Unified Modeling Language (UML) that allows specifying constraints over entities representing concepts from the application domain. The purpose of this paper is to describe a specific extension of OCL to model spatial constraints of Environmental Information Systems (EIS). These new features are applied to the agricultural spreading of organic matter. In this context, it is important to model a set of spatial constraints that define precisely where spreading can take place. For example, organic matters can never be spread inside certain natural areas. At present, some tools allow producing integrity checking mechanisms in different languages (Java, C#, SQL, etc.) from specifications of non-spatial constraints expressed in OCL. For instance, the SQL code generated by OCL2SQL can be used to check if a database verifies constraints or to forbid inserting data that do not verify them. In order to check spatial constraints in EIS, we implemented the “Spatial OCL” proposed in this paper into an extension of OCL2SQL. [Copyright &y& Elsevier]

Formal validation of UML models proves to be hardly realizable, due to the imprecise semantics of UML dynamic diagrams. To remedy that, we first present a technique for transforming UML statecharts into Petri nets. We develop afterwards, an approach based on the movement of the objects throughout the roles they play. This approach allows validation of the temporal logic properties translated from the OCL invariants, on the Petri nets derived from the UML models. System property validation is realized thanks to a prior initialization of the objects and exchanged messages between the communicating objects. A case study is given to illustrate the methodology. [ABSTRACT FROM AUTHOR]

This paper proposes a methodology and instrumentation infrastructure toward the reverse engineering of UML (Unified Modeling Language) sequence diagrams from dynamic analysis. One motivation is, of course, to help people understand the behavior of systems with no (complete) documentation. However, such reverse-engineered dynamic models can also be used for quality assurance purposes, They can, for example, be compared with design sequence diagrams and the conformance of the implementation to the design can thus be verified. Furthermore, discrepancies can also suggest failures in meeting the specifications. Due to size constraints, this paper focuses on the distribution aspects of the methodology we propose. We formally define our approach using metamodels and consistency rules. The instrumentation is based on Aspect-Oriented Programming in order to alleviate the effort overhead usually associated with source code instrumentation. A case study is discussed to demonstrate the applicability of the approach on a concrete example. [ABSTRACT FROM AUTHOR]

Abstract: The SQL (Structured Query Language) is currently available in most database management systems and is the focus of an intense standardization process resulting in the latest version of the SQL:2003 standard. Standards are fundamental, but often they are difficult to use, due to their lack of understandability and the occurrence of inconsistencies. An ontology is useful for clarifying the elements of a standard, along with their interrelationships, as well as for detecting inconsistencies. In this paper we propose an ontology for the object-relational features of the new SQL:2003 standard, formalized with UML 2.0 class diagrams and OCL well-formedness rules. The ontology is instantiated with an example in which most of the new object-relational features of the SQL:2003 standard are presented. [Copyright &y& Elsevier]

It is increasingly recognised that non-functional requirements should be considered at the earliest stages of system development. Unified modelling language (UML), as a standard, should therefore include notation to capture such requirements. Among these, timing has received considerable attention by the modelling community with several timed extensions of UML diagrams, a UML profile and tools. However, timing constraints are, generally, not captured in a satisfactory way during design. We propose to use UML's object constraint language (OCL) for this purpose, and provide a simple time enriched liveness template for OCL. We describe the benefits of using this template. Having verification in mind, several logic-based formalisms could be chosen to underly OCL. We consider a novel real-time logic of knowledge, and argue why logics of knowledge are useful and promising in this context. We illustrate our approach with a distributed real-time system. Future work and further benefits of the knowledge-based framework are discussed at the end of the paper. [ABSTRACT FROM AUTHOR]

At present, it is very difficult to develop a methodology that fulfills all criteria and comprises all security constraints in the successful design of data warehouses. If that methodology were developed, its complexity would hinder its success. The solution, therefore, would he an approach in which techniques and models defined by the most accepted model standards were extended by integrating the necessary security aspects that at this moment in time are not covered by the existing methodologies. In this paper, we will focus on solving confidentiality problems in the conceptual modelling of data warehouses by defining a profile using the UML 2.0 extensibility mechanisms. In addition, we define an OCL extension that allows us to specify the security constraints of the elements in conceptual modelling of data warehouses and we apply this profile to an example. [ABSTRACT FROM AUTHOR]

The eXtensible Markup Language (XML) is rapidly becoming the industry standard format for exchanging information across the networks. The validity of XML documents is very important for users and/or applications that consume them. While Document Type Definition (DTD) and XML Schema can be used to specify and validate the syntax of XML documents, they cannot specify or validate "semantic" constraints such as dynamic value constraints and inter-relationship constraints among element or attribute's values/presence. We propose a new XML constraint language -- eXtensible Constraint Markup Language (XCML) for specifying XML semantic constraints that are either assertion-based or rule-based. It is much more expressive than the existing XML constraint languages by supporting both dynamic constraints and inter-relationship constraints. We also propose a visual modeling framework of XCML constraints using Object Constraint Language (OCL) of Unified Modeling Language (UML), which automates the generation of XCML and XML Schema instance documents. The framework has been implemented with reusable XSLT stylesheets. The generated XML Schema document is used for syntactic validation. The generated XCML document is further transformed to an XSLT stylesheet by a reusable stylesheet. The transformed stylesheet is then used for semantic validation. The technologies demonstrated here can be used in XML data management, data warehousing, and decision support systems for various industry domains including healthcare information technology and E-Commerce. [ABSTRACT FROM AUTHOR]

We study the testing and certification of UML and OCL models as supported by the validation tool USE. We extend the available USE features by introducing a language for defining properties of desired snapshots and by showing how such snapshots are generated. Within the approach, it is possible to treat test cases and validation cases. Test cases show that snapshots having desired properties can be constructed. Validation cases show that given properties are consequences of the original UML and OCL model. [ABSTRACT FROM AUTHOR]

A large part of software development these days deals with building so-called Web applications. Many of these applications are data-base-powered and exhibit a page layout and navigational structure that is close to the class structure of the entities being managed by the system. Also, there is often only limited application-specific business logic. This makes the usual three-tier architectural approach unappealing, because it results in a lot of unnecessary overhead. One possible solution to this problem is the use of model-driven architecture (MDA). A simple platform-independent domain model describing only the entity structure of interest could be transformed into a platform-specific model that incorporates a persistence mechanism and a user interface. Yet, this raises a number of additional problems caused by the one-way, multi-transformational nature of the MDA process. To cope with these problems, the authors propose the notion of a model-driven runtime (MDR) environment that is able to execute a platform-independent model for a specific purpose instead of transforming it. The paper explains the concepts of an MDR that interprets OCL-annotated class diagrams and state machines to realize Web applications. It shows the authors' implementation of the approach, the Infolayer system, which is already used by a number of applications. Experiences from these applications are described, and the approach is compared to others. [ABSTRACT FROM AUTHOR]

The Object Constraint Language (OCL) was introduced as part of the Unified Modeling Language (UML). Its main purpose is to make UML models more precise and unambiguous by providing a constraint language describing constraints that the UML diagrams alone do not convey, including class invariants, operation contracts, and statechart guard conditions. There is an ongoing debate regarding the usefulness of using OCL in UML-based development, questioning whether the additional effort and formality is worth the benefit. It is argued that natural language may be sufficient, and using OCL may not bring any tangible benefits. This debate is in fact similar to the discussion about the effectiveness of formal methods in software engineering, but in a much more specific context. This paper presents the results of two controlled experiments that investigate the impact of using OCL on three software engineering activities using UML analysis models: detection of model defects through inspections, comprehension of the system logic and functionality, and impact analysis of changes. The results show that, once past an initial learning curve, significant benefits can be obtained by using OCL in combination with UML analysis diagrams to form a precise UML analysis model. But, this result is however conditioned on providing substantial, thorough training to the experiment participants. [ABSTRACT FROM AUTHOR]

The KeY system allows for the integrated informal and formal development of object-oriented Java software. In this paper we report on a major industrial case study involving safety-critical software for the computation of a particular kind of railway timetable used by train conductors. Our case study includes formal specification of requirements both on the analysis and the implementation level. Particular emphasis in our research is placed on the challenge to make authoring and maintenance of formal specifications easier. We demonstrate that the technique of specification patterns as implemented in KeY for the language OCL yields significant improvements. [ABSTRACT FROM AUTHOR]

The objective it to present a technique that facilitates cross-validation of software metrics for component-based development. The technique is illustrated with a cross-validation experiment for a suite of reusability metrics for component based design published in the literature. These metrics were originally proposed using a semi-formal notation, namely a combination of mathematical formulae with natural language descriptions for their elementary parts. They were then computed using proprietary tools. By contrast, we present a formalization for the metrics suite that combines the UML 2.0 metamodel with OCL. This technique provides a formal, portable and executable definition of the metrics set that can be used to perform cross-validations of the metrics suite, such as the one presented in this paper. The ability to independently replicate metrics validation experiments is essential to the scientific progress of component based software engineering. [ABSTRACT FROM PUBLISHER]

KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and object-oriented development techniques are applied in an integrated manner. Formal specification is performed using the Object Constraint Language (OCL), which is part of the UML standard. KeY provides support for the authoring and formal analysis of OCL constraints. The target language of KeY based development isJava Card DL, a proper subset ofJavafor smart card applications and embedded systems. KeY uses a dynamic logic forJava Card DLto express proof obligations, and provides a state-of-the-art theorem prover for interactive and automated verification. Apart from its integration into UML based software development, a characteristic feature of KeY is that formal specification and verification can be introduced incrementally. [ABSTRACT FROM AUTHOR]

This paper describes methods and tools for safety analysis of UML statechart specifications. A comprehensive set of general safety criteria including completeness and consistency is applied in automated analysis. Analysis techniques are based on OCL expressions, graph transformations and reachability analysis. Two canonical intermediate representations of the statechart specification are introduced. They are suitable for straightforward implementation of checker methods and for the support of the proof of the correctness and soundness of the applied analysis. One of them also serves as a basis of the metamodel of a variant of UML statecharts proposed for the specification of safety-critical control systems. The analysis is extended to object-oriented specifications. Examples illustrate the application of the checker methods implemented by an automated tool-set. [Copyright &y& Elsevier]

In this paper, we propose a development framework that extends the scope of structured review by supplementing the structured review with model-based verification. The proposed approach uses the Unified Modeling Language (UML) as a modeling notation. We discuss a set of correctness arguments that can be used in conjunction with format verification and validation (V&V) in order to improve the quality and dependability of systems in a cost-effective way. Formal methods can be esoteric; consequently, their large scale application is hindered. We propose a framework based on the integration of lightweight formal methods and structured reviews. Moreover, we show that structured reviews enable us to handle aspects of V&V that cannot be fully automated. To demonstrate the feasibility of our approach, we have conducted a study on a security-critical system-a patient document service (PDS) system. [ABSTRACT FROM AUTHOR]

A type inference system and a big-step operational semantics for expressions of the “Object Constraint Language” (OCL), the declarative and navigational constraint language for the “Unified Modeling Language” (UML), are provided; the account is mainly based on OCL 1.4/5, but also includes the main features of OCL 2.0. The formal systems are parameterised in terms of UML static structures and UML object models, which are treated abstractly. It is proved that the operational semantics satisfies a subject reduction property with respect to the type inference system. Proceeding from the operational semantics and providing a denotational semantics, pure OCL 2.0 expressions are shown to exactly represent the primitive recursive functions, whereas pure OCL 1.4/5 expressions are Turing complete. [ABSTRACT FROM AUTHOR]