This file was created with JabRef 2.1. Encoding: Cp1252 @INPROCEEDINGS{Baruzzo2006, author = {Andrea Baruzzo and Marco Comini}, title = {{S}tatic {V}erification of {UML} {M}odel {C}onsistency}, year = {2006}, month = {October}, abstract = {In a UML model, different aspects of a system are covered by different types of diagrams and this bears the risk that an overall system specification becomes inconsistent or incomplete. Hence, it is important to provide means to check the consistency and completeness of a UML model. Many approaches for model validation and verification rely on generation of suitable code which dynamically (i.e., at run-time) checks the validity of OCL constraints. This approach has several well-known drawbacks. For example, it cannot generally guarantee that a constraint will never be violated, unless an infinite number of tests is performed. On the other hand, even more desirable static approaches are not immune from weaknesses. The techniques based on model checking suffer from the state explosion problem and thus cannot scale to most system sizes. Moreover, the static approach is in general undecidable. In this paper we propose a static verification framework based of Abstract Interpretation techniques, a theory of approximation of mathematical structures. This framework, by using OCL constraints together with Class Diagrams, certifies that the dynamic part (Sequence Diagrams) of the model is satisfied. Our approach keeps the advantages of static verification and, at the same time, avoids the weaknesses of the other mentioned methods as it does not require users to build test scenarios and also it can make undecidable methods decidable, up to a specified level of precision.}, crossref = {Hearnden2006}, owner = {jgsuess}, timestamp = {2006.10.20} } @INPROCEEDINGS{Bouquet2006, author = {Fabrice Bouquet and Stéphane Debricon and Bruno Legeard and Jean-Daniel Nicolet}, title = {{E}xtending the {U}nified {P}rocess with {M}odel-{B}ased {T}esting}, year = {2006}, month = {October}, abstract = {The Unified Process (UP) is a software development technique that includes modeling of specifications and testing workflow. This workflow is achieved by information interpretation of specification to produce manual tests. In this paper, we extend the UP with model-based testing (MBT) where models resulting of the UP will be used for MBT. We describe how model-based testing introduces new test design activities in parallel with the application design activities. We give guidelines to derive the test model from the analysis model produced by the UP. We illustrate this tailored process with the example of a Geneva State taxation.}, crossref = {Hearnden2006}, keywords = {Unified Process, Model-Based Testing, Class Diagrams, Statecharts, OCL, Model specialization}, owner = {jgsuess}, timestamp = {2006.10.19} } @INPROCEEDINGS{Engels2006, author = {Gregor Engels and Baris Güldali and Marc Lohmann}, title = {{T}owards {M}odel-{D}riven {U}nit {T}esting}, year = {2006}, month = {October}, abstract = {The Model-Driven Architecture (MDA) approach for constructing software systems advocates a stepwise refinement and transformation process starting from high-level models to concrete program code. In contrast to numerous research efforts that try to generate executable function code from models, we propose a novel approach termed model-driven monitoring. On the model level the behavior of an operation is specified with a pair of UML composite structure diagrams (visual contract), a visual notation for pre- and post-conditions. The specified behavior is implemented by a programmer manually. An automatic translation from our visual contracts to JML assertions allows for monitoring the hand-coded programs during their execution. In this paper we present an approach to extend our model-driven monitoring approach to allow for model-driven unit testing. In this approach we utilize the generated JML assertions as test oracles. Further, we present an idea how to generate sufficient test cases from our visual contracts with the help of model-checking techniques.}, crossref = {Hearnden2006}, owner = {jgsuess}, timestamp = {2006.10.20} } @INPROCEEDINGS{Giese2006, author = {Holger Giese and Sabine Glesner and Johannes Leitner and Wilhelm Schäfer and Robert Wagner}, title = {{T}owards {V}erified {M}odel {T}ransformations}, year = {2006}, month = {October}, abstract = {Model-driven software development (MDD) is seen as a promising approach to improve software quality and reduce production costs significantly. However, one of the problems in using MDD especially in the area of safety-critical systems is the lack of verified transformations. The verification of crucial safety properties on the model level is only really useful, if the automatic code generation is also guaranteed to be correct, i.e., the verified properties are guaranteed to hold also for the generated code. This particularly means to check semantic equivalence, at least to a certain extent between the model specification and the generated code. This paper addresses the problem of verifying that a given transformation ensures semantic equivalence between an arbitrary model in a given model specification language and the resulting programming language code. While the presented approach ensures that the transformation algorithm is correct, existing related work is restricted on verifying only the correctness of a particular transformation result.}, crossref = {Hearnden2006}, owner = {jgsuess}, timestamp = {2006.10.20} } @INPROCEEDINGS{Gupta2006, author = {Atul Gupta}, title = {{A}utomated {O}bject’s {S}tatechart {G}eneration and {T}esting from {C}lass {M}ethod {C}ontracts}, year = {2006}, month = {October}, abstract = {The link between an object’s class specifications and UML statechart is rather informal and poses consistency issues during software evolution. We address this issue by proposing a connection between class diagram and statechart in a lock-step fashion, which leads to a coherent design for better development, testing, and maintenance of the software system. In this paper, we describe an approach for generating a statechart for an object from its method contracts.We then show how the generated object statechart can be used for performing automated testing at unit level. We illustrate the approach using a simple example and discuss its effectiveness as a V&V step during software evolution.}, crossref = {Hearnden2006}, owner = {jgsuess}, timestamp = {2006.10.20} } @INPROCEEDINGS{Kuester2006, author = {Jochen M. Küster and Mohamed Abd-El-Razik}, title = {{V}alidation of {M}odel {T}ransformations - {F}irst {E}xperiences using a {W}hite {B}ox {A}pproach}, year = {2006}, month = {October}, abstract = {Validation of model transformations is important for ensuring their quality. Successful validation must take into account the characteristics of model transformations and develop a suitable fault model on which test case generation can be based. In this paper, we report our experiences in validating a number of model transformations and propose three techniques that can be used for constructing test cases.}, crossref = {Hearnden2006}, owner = {jgsuess}, timestamp = {2006.10.20} } @INPROCEEDINGS{Lano2006, author = {Kevin Lano}, title = {{U}sing {B} to verify {UML} {T}ransformations}, year = {2006}, month = {October}, abstract = {This paper describes the use of the B formal method to verify semantic properties of UML graphical models, and the correctness of transformations on these models.}, crossref = {Hearnden2006}, owner = {jgsuess}, timestamp = {2006.10.19} } @INPROCEEDINGS{Toni2006, author = {Toni Jussila, Jori Dubrovin, Tommi Junttila, Timo Latvala, Ivan Porres}, title = {{M}odel {C}hecking {D}ynamic and {H}ierarchical {UML} {S}tate {M}achines}, year = {2006}, month = {October}, abstract = {This paper presents a technique to model check UML specifications by translating UML models to the model checker SPIN. Our models consist of active UML classes, whose behavior is defined by hierarchical state machines. The intended application is to find errors in protocols communicating using asynchronous message passing. Compared to previous efforts using a similar approach, our novel points are the following. First, we consider a subset of UML that in our opinion is expressive enough for protocol models but allows a simpler translation to SPIN than existing work. Preliminary analysis of simple industrial models support our conclusions on the expressivity of our UML subset. Second, we present a powerful action language that is still amenable to automatic analysis. The action language is used to specify the effects of transitions, which may include dynamic creation of new objects. Finally, we discuss an even simpler SPIN translation for flattened UML state machines and compare it to the translation that supports hierarchy.}, crossref = {Hearnden2006}, owner = {jgsuess}, timestamp = {2006.10.20} } @INPROCEEDINGS{Whittle2006, author = {Jon Whittle}, title = {{V}alidating {T}ransformations on {D}omain-{S}pecific {M}odels}, year = {2006}, address = {4400 University Drive Fairfax, VA 22030-4444, USA}, month = {Oct}, organization = {George Mason University}, note = {Keynote Address}, abstract = {Model-Driven Software Development brings new hopes and new challenges for the V&V of safety- and mission-critical systems. On the one hand, automated model transformations have the potential to reduce testing effort since a significant amount of code can be autogenerated. On the other hand, for practical systems, the transformations themselves may contain errors and therefore need to be validated. This talk will present work on verifying key properties of auto-generated code by augmenting transformations to output not only code, but also information that can be used to show the correctness of the code. These ideas were implemented in the Autofilter code generator at NASA Ames Research Center. Autofilter generates key portions of flight control software based on a domain-specific model. As an experiment, Autofilter was used to generate code equivalent to that flown on the Deep Space I probe. The talk discusses techniques for validating Autofilter’s code generator and will offer hints at future research directions.}, crossref = {Hearnden2006}, owner = {jgsuess}, timestamp = {2006.11.18} } @PROCEEDINGS{Hearnden2006, title = {{M}o{D}e{V}²a: {M}odel {D}evelopment, {V}alidation and {V}erification.}, year = {2006}, editor = {David Hearnden and Jörn Guy Süß and Benoît Baudry and Nicolas Rapin}, publisher = {Le Commissariat à l'Energie Atomique - CEA}, month = {Oct}, organization = {University of Queensland}, abstract = {The MoDeVa series of workshops offers a forum for researchers and practitioners with varying backgrounds to discuss new ideas concerning links between modelbased design and model-based validation. It aims to introduce models as a link between the theoretic foundations of Validation and Verification, and the practice of model-based testing. Also, it seeks to critically examine the pivotal parts of the Model-Driven Architecture paradigm: Models, Metamodels and Transformations. MDA and its related approaches (DSL, MDE, . . . ) primarily revolve around manual refinement and automated transformation of models. This approach is successful at quickly generating results. However, it is difficult to gauge the quality of those results. Is the result of a transformation really what the user intended? Does the computed result of a transformation really conform with its specified result? Such questions about intended and specified behaviour usually delineate the domain of Validation and Verification (V&V). V&V is an established area of research, and a transfer of ideas between V&V and MDA might help to improve quality and reliability of MDA and induce a new conceptual way of thinking in established V&V. The emergence of model-based testing can be seen as a first result of such a transfer. However, we believe that to go beyond model-based testing and take a truly model-driven-development approach to V&V would yield even greater benefits. This workshop has fostered a discussion in this direction presenting work related on the following topics: - The application of V&V using MDA - The application of ‘traditional’ V&V to MDA - The integration of testing tools and MDA tools - The application of V&V to MDA transformations - The application of ‘novel’ V&V to MDA - V&V due to the evolution of models on any level - The extension of UML in a tool-independent way to allow V&V}, keywords = {workshop, models, 2006, MDA, verification, validation, D2, D2.2, D2.4, D.2.5, D2.10, F3.1}, owner = {jgsuess}, timestamp = {2006.10.19}, url = {http://modeva.itee.uq.edu.au} } @comment{jabref-meta: selector_journal:} @comment{jabref-meta: selector_author:} @comment{jabref-meta: selector_keywords:} @comment{jabref-meta: selector_publisher:} @comment{jabref-meta: groupsversion:3;} @comment{jabref-meta: groupstree: 0 AllEntriesGroup:; 1 KeywordGroup:omg\;0\;year\;2005\;0\;0\;; }