@proceedings {BaruzzoC07c,
	title = {A Methodology for UML Models V\&V},
	journal = {Proceedings of First International Conference on Software Testing, Verification, and Validation},
	year = {2008},
	pages = {513{\textendash}516},
	publisher = {IEEE Computer Society},
	abstract = {The introduction of UML models in the software life cycle poses new issues and challenges that are not adequately supported by current state-of-the-art development tools, es- pecially concerning V\&V activities. Indeed, every tool usually focuses on a small set of specialized activities, failing to provide a satisfactory (general purpose) V\&V framework.
In this paper we propose a methodology which allows a seamless integration of V\&V into a UML-based development environment. The methodology exploits a set of sup- porting tools designed to be integrated in a unified frame- work. We believe that such proactive collaboration between tools can reduce significantly both effort and time required to tackle consistency, correctness, quality and long-term maintainability of UML models, increasing the development productivity and the overall quality of the delivered system.},
	isbn = {978-0-7695-3127-4},
	author = {Andrea Baruzzo and Marco Comini}
}
@proceedings {BallisBC07b,
	title = {A Minimalist Visual Notation for Design Patterns and Antipatterns},
	journal = {5th International Conference on Information Technology: New Generations},
	year = {2008},
	pages = {51{\textendash}56},
	publisher = {IEEE Computer Society},
	abstract = {Achieving a quality software system requires UML designers to have a good understanding of both design patterns and antipatterns. Unfortunately, UML models for real systems tend to be huge and hard to manage, especially for models automatically generated from source code. Thus, it would be advisable to have tools to automatically identify particular instances of patterns. So, a formal language to express them is needed. However, a textual formalization of such a language is barely usable by UML practitioners. In this paper we propose a visual notation obtained by adding to UML as few graphical elements as possible in order to express both patterns and antipatterns (with the needed formality). This approach has low cognitive load so is easily usable by practitioners but is still rigorous enough for implementation. This notation will be exploited by a GUI front-end for a prototypical tool (that we have recently developed) which is able to discover (anti)patterns in models.
In [3], we proposed a rule-based matching algorithm to identify all instances of a pattern in the graph which underlies the designers{\textquoteright} diagrams. A pattern is given in a general textual language that can express at the same time patterns and antipatterns. However, a formal textual specification is hard to use by UML practitioners. This work was just our first step towards a more ambitious goal: providing a pattern-matching tool that works with a graphical language which extends UML adding as few graphical primitives as possible, yet at the same time retaining the needed precision to be effectively implementable. In this paper we propose such a visual notation. As the additional primitives are really few and intuitive, we believe that this approach involves a reduced cognitive load for the UML designer. Moreover, we developed an algorithm to convert the visual representation of a pattern to an equivalent textual description in terms of the language proposed in [3]. This description can eventually be fed to the prototypical tool that we have developed.},
	doi = {10.1109/ITNG.2008.227},
	author = {Demis Ballis and Andrea Baruzzo and Marco Comini}
}
@mastersthesis {Baruzzo08,
	title = {A Unified Framework for Automated UML Model Analysis},
	year = {2008},
	school = {Dipartimento di matematica e Informatica},
	type = {phd},
	author = {Andrea Baruzzo}
}
@unpublished {BaruzzoC07,
	title = {A Framework for Computer Aided Consistency Verification of UML Models},
	year = {2007},
	note = {\bibURL{http://www.dimi.uniud.it/comini/Papers/FramCAConVerUML/FramCAConVerUML.pdf}.},
	abstract = {In a UML model, different aspects of a system are covered by different diagrams and this bears the risk that an overall specification becomes inconsistent or incomplete. Hence, it is important to provide means to check the consistency and completeness of a model.

In this paper we propose a static verification framework which checks the mutual consistency of class, statechart, and sequence diagrams (without relying on existent code).

Our approach aims to keep the advantages of static verification and, at the same time, to avoid the weaknesses of other methods, either static or dynamic, which depend on non-UML formalisms. Indeed it does not require developers further (heavy) cognitive load and, moreover, does not force them to keep this external specifications synchronized with the model.},
	author = {Andrea Baruzzo and Marco Comini}
}
@proceedings {BallisBC07,
	title = {A rule-based method to match Software Patterns against UML Models},
	journal = {The 8th International Workshop on Rule-Based Programming (RULE {\textquoteright}07)},
	year = {2007},
	pages = {239{\textendash}248},
	publisher = {Elsevier Science Publishers},
	address = {North Holland},
	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 barely tractable by the designer. When the model grows, it is likely that the architectural integrity will be compromised by extensions and bug-fixing operations. Hence, it is important to provide means to help designers to search in big models for particular instances of some variable schema of UML models (design patterns) they construct. This can help them both to find potential problems in the architecture design and to ensure that intended architectural choices had not been broken by mistake. In this paper we propose a rule-based method to find matches of design patterns into a UML model. The method is general enough to tackle most patterns and antipatterns.},
	keywords = {Pattern Matching, Rule-based domain specific language, UML Design Patterns, UML formal specification},
	author = {Demis Ballis and Andrea Baruzzo and Marco Comini}
}
@unpublished {BaruzzoC07b,
	title = {Toward a Unified Framework for Quality and Consistency Verification of UML Models},
	year = {2007},
	note = {\bibURL{http://www.dimi.uniud.it/comini/Papers/FrameworkQualConsUML/FrameworkQualConsUML.pdf}.},
	abstract = {Model-Driven Development (MDD) is an emergent approach to software engineering which is based on the systematic use of software modeling as a primary form of expression. The central focus in MDD is on models, as opposed to source code in the traditional conception of software development. However the introduction of models in the software life cycle poses new issues and challenges that current state-of-the-art development tools do not support adequately.

In this paper we investigate some of these challenges, taking into account the role played by models. Then we propose a unified framework which integrates different verification methods with the intent to check (UML) models against consistency issues and design defects. Our approach aims to integrate traditional techniques with model-based ones, keeping the advantages of both static and dynamic verification methods in order to increase the proficiency of the MDD activities.},
	author = {Andrea Baruzzo and Marco Comini}
}
@proceedings {BaruzzoC06,
	title = {Checking UML Model Consistency},
	journal = {Proceedings of CILC 2006 - Convegno Italiano di Logica Computazionale},
	year = {2006},
	pages = {1{\textendash}15},
	abstract = {UML is nowadays a de-facto standard for design and development of (object-oriented) software. With version 2.0 UML has achieved a more precise formal semantics. The same happened to OCL, a specification language which is an integral part of UML that allows to embed software contracts in the model.
In this work we propose an approach for a static verification of consis- tency of UML models which relies on OCL constraints. 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 drawbacks. For example, it cannot generally guarantee that a constraint will never be violated, unless an infinite number of tests is performed. Also the generation of just a significative finite subset is not so feasible because, on one hand, a considerable manual effort is needed even to produce a single test scenario and, on the other hand, test-case generation is well-known to be a hard problem.
On the other hand, static approaches based on model checking suffer of the state explosion problem and thus cannot scale to real system sizes. In this paper we propose a static verification technique that, by using OCL constraints together with class diagrams, certifies that the dynamic part of the model is satisfied. This encompasses the weaknesses of the other mentioned methods as it does not require users to build test sce- narios and also performs the verification of all system properties at the same time.},
	author = {Andrea Baruzzo and Marco Comini}
}
@proceedings {BaruzzoC06a,
	title = {Static Verification of UML Model Consistency},
	journal = {MoDeV{$^2$}a: Model Development, Validation and Verification},
	year = {2006},
	month = {October},
	pages = {111{\textendash}126},
	publisher = {University of Queensland},
	abstract = {UML is nowadays a de-facto standard for design and development of (object-oriented) software. With version 2.0 UML has achieved a more precise formal semantics. The same happened to OCL, a specification language which is an integral part of UML that allows to embed software contracts in the model.
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. In this work we propose an approach for a static verification of consistency of UML models which relies on OCL constraints.
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 drawbacks. For example, it cannot generally guarantee that a constraint will never be violated, unless an infinite number of tests is performed. Also the generation of just a significative finite subset is not so feasible because, on one hand, a considerable manual effort is needed even to produce a single test scenario and, on the other hand, test-case generation is well-known to be a hard problem.
On the other hand, static approaches based on model checking suffer of the state explosion problem and thus cannot scale to most system sizes. In this paper we propose a static verification technique that, by using OCL constraints together with Class Diagrams, certifies that the dy- namic part of the model is satisfied. This encompasses the weaknesses of the other mentioned methods as it does not require users to build test scenarios and also performs the verification of all system properties at the same time.},
	keywords = {OCL, UML diagrams, UML models, Validation, Verification},
	url = {http://modeva.itee.uq.edu.au},
	author = {Andrea Baruzzo and Marco Comini},
	editor = {Hearnden, D. and S{\"u}{\ss}, J. G. and Benoit Baudry and Rapin, N.}
}
