Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Modeling and Analyzing Softwar...

Modeling and Analyzing Software Behavior in UML

Ivan Porres, Modeling and Analyzing Software Behavior in UML. TUCS Dissertations 34. Turku Centre for Computer Science, 2001.

Abstract:

<p>The purpose of a software model is to represent and convey the most
important requirements and design decisions of a software system. Currently, the
most popular software modeling language is the Unified Modeling Language
(UML). In this thesis we study methods to analyze the behavior described in a
UML model. We can use the methods presented in the thesis to analyze and
assure the quality of the models and detect some design errors before starting
their implementation.</p>

<p>We focus on the behavioral aspects of UML since we consider that they have
not been studied well enough yet. We have chosen the two diagrams that we
consider are key for describing behavior in UML: use case diagrams and
statecharts. Use case diagrams show the system as a black box, from the point of
view of a system. Statechart diagrams can show each single object in our model
as a white box and describe its internal behavior in full detail.</p>

<p>We complement the use case diagrams by providing formal documents
similar to specifications or programs, called contracts, which regulate the
behavior of the actors involved. A contract is written in the refinement calculus as
introduced by Back and von Wright, and thus it can be analyzed mathematically.
In particular, we can check whether a specific actor can achieve given goals with
the contract, in spite of possibly conflicting behavior with other actors. In order to
analyze a contract we define the precise meaning of each statement we use as
weakest precondition predicate transformers.</p>

<p>In the thesis we also discuss a complete formalization of the semantics of
UML statecharts. The formalization is given in terms of an operational semantics
and it can be used as the basis for code generation, simulation and verification
tools for UML statechart diagrams. We use this formalization of statecharts in the
vUML tool, a prototype tool for model-checking UML models. The vUML tool
supports concurrent and distributed models containing active objects and
synchronous and asynchronous communication between objects. To use vUML,
the behavior of each object must be specified using one statechart.</p>

<p>We also present an extension of UML statecharts that can be useful to model
real-time and hybrid systems. This extension consists of just a new model
element: the continuous action. A continuous action can be used to model a real-
time clock or a physical behavior described as a function of time. We formalize
continuous actions using the action systems language of the refinement calculus.
We show how to use this new formalism to analyze safety properties of hybrid
statecharts.</p>

<p>In conclusion, the thesis shows how to bridge an informal diagram notation
such as UML with two existing formal methods: the refinement calculus and
model checking. In this way, we obtain the benefits of a graphical language but
we are still able to rigorously analyze the behavior of the models.</p>

Files:

Full publication in PDF-format

BibTeX entry:

@PHDTHESIS{phdPorres01a,
  title = {Modeling and Analyzing Software Behavior in UML},
  author = {Porres, Ivan},
  number = {34},
  series = {TUCS Dissertations},
  school = {Turku Centre for Computer Science},
  year = {2001},
  keywords = {UML, Software Engineering, Formal Methods, Refinement Calculus, Modelcheking},
  ISBN = {951-29-2169-3},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Edit publication