<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>A New Approach to Reliable, yet Flexible Software</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Abbas Rasoolzadegan</string-name>
          <email>rasoolzadegan@aut.ac.ir</email>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Intelligent Systems Laboratory (</institution>
        </aff>
      </contrib-group>
      <abstract>
        <p>Developing reliable, yet flexible software is a hard problem. Formal methods take a precise approach to software development, delivering reliable software; however, in addition to high cost involvements, they require a level of expertise that is not common in commercial development communities. These limitations lead to decreasing their practicality. Semi-formal methods, which are widely used in practical large-scale software development, do not take a rigorous approach to reliability of software in development. Investigation of advantages and limitations of semi-formal and formal methods, theoretically (by surveying the literature) and empirically (by defining a suitable case study), shows that combination of both methods ensures achieving high quality models which in turn lead to flexibility and more reliable software. This work proposes a new approach to integrate formal (Object-Z) and semi-formal (UML) notations using a bidirectional, precise, and consistent meta-model-based transformation. Accordingly, software is initially modeled using Object-Z. These formal models, along with formal refinement ensure reliability. With an iterative and evolutionary approach, formal models are visualized in UML. Applying design patterns on visualized models improves flexibility. The improved models are then re-formalized.</p>
      </abstract>
      <kwd-group>
        <kwd>UML</kwd>
        <kwd>Object-Z</kwd>
        <kwd>design patterns</kwd>
        <kwd>meta-model-based transformation</kwd>
        <kwd>model transformation</kwd>
      </kwd-group>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>-</title>
      <p>
        Software permeates our daily life. There is probably no other human-made material
which is more omnipresent than software in our modern society. It has become a
crucial part of many aspects of society. Size and complexity of software systems have
grown dramatically during the past few decades, and the trend will certainly continue
in the future. Because of this ever-increasing dependency, software failures can lead
to serious, even fatal, consequences in safety-critical systems as well as in normal
business [
        <xref ref-type="bibr" rid="ref7">7</xref>
        ]. Moreover, rapid technological developments pervade every aspect of
daily life, having direct effect on the software we use. Every element of the software s
operational environment is in a state of constant flux [
        <xref ref-type="bibr" rid="ref32">32</xref>
        ]. Contemporary literature
recognizes the central role of reliability and flexibility in software development.
      </p>
      <p>
        Studies show that the major causes of most software failure are imprecise and
incomplete understanding of customer requirements as well as lack of precise, careful,
and comprehensive elicitation, specification, analysis, validation, and verification of
them during Requirements Engineering (RE) in software development cycle [
        <xref ref-type="bibr" rid="ref3">3</xref>
        ].
Moreover, mainstream software development, with its recurring practice of trial and
error, already suffers from its premature insistence on code and program testing. The
problem is that code is expensive; it has too much detail, and is not at the right level
of abstraction to help thinking about the problem and the design of its solution.
      </p>
      <p>
        The increasing importance of developing reliable and flexible software beside
increasing necessity of RE as well as need for further abstraction lead to increasing
use of various types of models [
        <xref ref-type="bibr" rid="ref3">3</xref>
        ], [
        <xref ref-type="bibr" rid="ref31">31</xref>
        ]. Models are used at different phases of
software development, ranging from requirements to detailed design for specification,
analysis, validation, and verification of customer requirements, problems and also
design of their solutions. This is the idea behind Model-Driven Software Engineering
(MDSE) [
        <xref ref-type="bibr" rid="ref27">27</xref>
        ], an approach that advocates models, rather than code, as the primary
artifacts of software development. Model transformation and model refinement have
key roles in MDSE. Model transformation includes model-to-text transformation to
generate code from models, text-to-model transformations to parse textual
representations to model representations, model extraction to derive higher-level
models from legacy code, and model-to-model transformations to normalize, weave,
optimize, and refactor models, as well as to translate between modeling languages.
The fact that models may have different levels of abstraction gives a basis for a
stepwise approach to software development: abstract models are refined into more
concrete ones in a stepwise manner, where each step carries some design decisions.
      </p>
      <p>
        Semi-formal methods (SFMs) using semi-formal languages have a visual nature,
and it is this, together with their pragmatic approach to development, that explains
their popularity. They have emerged from a need to abstract away from the details of
code and to visualize the overall system structure and behavior. The main strengths of
semi-formal techniques include: intuitive and widely known notations and
methodological support emphasizing problem decomposition. Lack of a sound
mathematical basis is the major weakness of SFMs which in turn leads to different
interpretations [
        <xref ref-type="bibr" rid="ref6">6</xref>
        ], [
        <xref ref-type="bibr" rid="ref19">19</xref>
        ] as well as ambiguous, imprecise, and inconsistent
specification. Misunderstandings in the specification lead to against-user-expectation
behavior of the software. SFMs also suffer from lack of means for mechanical
analysis.
      </p>
      <p>
        Formal methods (FMs) using formal languages provide the software with precise,
unambiguous, and abstract specification during development cycle. In the next design
steps, required details are gradually added to initial specification through an
evolutionary formal refinement process [
        <xref ref-type="bibr" rid="ref3">3</xref>
        ], [
        <xref ref-type="bibr" rid="ref31">31</xref>
        ]. FMs are based on prediction and
calculation with sound mathematical theories. They are utilized throughout software
development life cycle [
        <xref ref-type="bibr" rid="ref13">13</xref>
        ] for precise specification, complete analysis, and rigorous
verification and validation of software requirements. However, they require expertise.
So, customers, users, analyzers, and designers (who do not, necessarily, master
enough their complex mathematical concepts) are unable to analyze and validate the
formal models. Therefore, FMs have not been taken up by industry. They have been
embraced only in domains where reliability is absolutely crucial, such as
safetycritical, security-critical, and high integrity systems [
        <xref ref-type="bibr" rid="ref6">6</xref>
        ] because of their high up-front
cost. Other kinds of systems, however, are driven by other priorities, such as time to
market, feature count, and cost of production. The problem with formal methods, as
they stand today, is that they clearly conflict with such priorities. They also suffer
from lack of methodological and tool supports.
      </p>
      <p>We conclude that FMs and SFMs have some unique advantages and limitations.
Using only one of them as the sole approach leads not to reliable and flexible software
but to reliable or flexible software. So, we aim to supplement the semi-formal
methods with formal ones in order to introduce rigor in the development, and to
sweeten formal methods usage with visualization. Such an integration results in
developing software with the desired quality.</p>
      <p>
        We have taken a non-trivial system, namely the multi-lift system as a case study
[
        <xref ref-type="bibr" rid="ref34">34</xref>
        ]. This system is a commonly used test bed to demonstrate the expressive power of
various modeling languages in specifying concurrent reactive systems. It is not a
trivial case study because of the complexity caused by inherent concurrent interaction
in the system.
      </p>
      <p>Investigation of the advantages and limitations of semi-formal and formal methods,
theoretically (by surveying the literature) and empirically (by defining a suitable case
study) shows that combination of both methods would be necessary for precise and
complete requirements specification, validation, and verification as well as flexible
and reliable design in a practical approach. Such a combination ensures achieving
high quality models. More information about the details of the investigation
performed on the advantages and limitations of FMs and SFMs according to the
literature review and empirical experiments is publically accessible via
http://ceit.aut.ac.ir/islab/Researches/RE/Appendix.doc.</p>
      <p>
        We strongly believe that it is possible to integrate FMs into mainstream software
modeling practice. This can be done in a flexible and practical way, so that the
integration has an engineering value and is actually worth doing. There have been
many approaches that perform such integrations with very positive results. So, before
the work reported here even started, there was already strong evidence in favor of its
possibility. There are also different ways to achieve the goal of practicality [
        <xref ref-type="bibr" rid="ref1">1</xref>
        ]. So, we
aim to follow a rigorous approach to MDSE that is practical based on combining
semi-formal notations with formal modeling languages regarding to their advantages
and limitations. The rigor will be given by the use of formal models. The practicality
will be provided through application of semi-formal models which are accessible to a
wide range of developers who do not need to be formal methods experts. In fact, this
paper enables the construction of formal models from diagrams (formalizing) and vice
versa (visualization). To do so, this work proposes a precise, consistent, and complete
transformation between visual models in UML and formal models in Object-Z.
      </p>
      <p>This work emphasizes on the software behavior rather than its structure. In the
proposed approach, the formalism plays the key role, i.e., the software is initially
modeled using Object-Z. These formal models, along with formal refinement ensure
reliability. Then, with an iterative and evolutionary approach and in specific intervals,
software behavior is extracted from formal models to be visualized in UML.
Visualized behavior increases and facilitates the interactions among project
stakeholders (such as analyzers and designers), who are not, necessarily, familiar
enough with complex mathematical concepts of formal methods. This also provides
the possibility of applying design patterns on visualized behavior to improve its
flexibility. So potential errors and inconsistencies of the software behavior are
identified and, consequently, required changes are applied and a newly improved
version of the formal behavior is produced. The improved models are then
reformalized. The proposed approach is a practical step towards development of correct,
reliable, and flexible software.</p>
      <p>The rest of this paper is organized as follows: Section 2 defines the problem that
will be solved by the proposed approach. The goals and outputs of this work are also
expressed in this section. In section 3 the problem solving method is described, i.e. the
path towards solving the defined problem and achieving the promised goals is drawn.
Testing and evaluation method of the new approach is then presented. Finally, Section
4 discusses future work and draws some conclusions.
2</p>
    </sec>
    <sec id="sec-2">
      <title>Problem Definition</title>
      <p>The problem to be investigated by this work is defined in this section. Solving this
problem is a step towards developing reliable, yet flexible software. To do so, a new
approach based on integrating Object-Z and UML is proposed. Using FMMs as the
sole approach to software development leads to reliable software but with the
following issues:
1. There are different interpretations of the initial informal requirements by customer
and development team. There is also possibility of changing requirements during
software development. These issues end to production of a software in contrary
with the initial requirements. Figure 1 illustrates this problem. There are two
reasons for such an incorrect result: 1) there is no possibility of proving a perfect
match between actual informal requirements and initial formal specification ( ),
2) it is difficult to do validation in the interval because of the trouble in
understanding the formal models. So formal methods, certainly brings us to a result
that conforms to the initial formal specification (because of formal refinements),
however, it does not necessarily conform to the actual informal requirements.</p>
      <p>
        Visualization is an approach to solve this issue which leads to facilitate
requirements validation in the interval [
        <xref ref-type="bibr" rid="ref23">23</xref>
        ]. However, prototyping [
        <xref ref-type="bibr" rid="ref24">24</xref>
        ] is a better
solution for requirements validation. To do so, the formal specification should be
transformed so that its new form can be executed or animated [
        <xref ref-type="bibr" rid="ref17">17</xref>
        ], [
        <xref ref-type="bibr" rid="ref24">24</xref>
        ]
2. Even assuming that the initial formal specification exactly represents the actual
informal functional requirements of the customer, we still do not reach the software
with good enough quality of non-functional requirements such as reusability,
flexibility, scalability, and extendibility. There are two reasons for such an
unexpected result: 1) difficulty in utilizing the semi-formal and narrative
techniques of software engineering such as design patterns in the interval , 2)
inability of development team members such as analyzers and designers in
understanding complex mathematical concepts of formal languages. This work
aims to solve this problem. To do so, a new approach is suggested to improve
software development process by combining Object-Z and UML to achieve high
quality models of specification and design which in turn lead to more reliable and
flexible software. Figure 2 illustrates a schematic view of the new proposed
approach. Visualization facilitates understanding of the formal models and
subsequently provides possibility of interaction with stakeholders, who are not
necessarily familiar enough with complex mathematical concepts of formalism. It
also simplifies using the narrative techniques of software engineering such as
design patterns during software development process.
      </p>
      <p>
        Software includes two aspects: structure (static) and behavior (dynamic) [
        <xref ref-type="bibr" rid="ref24">24</xref>
        ], [
        <xref ref-type="bibr" rid="ref29">29</xref>
        ].
The proposed approach concentrates on software behavior. It facilitates analyzing and
validating the behavioral aspect of formal models of software by visualization.
Visualization prepares an appropriate ground to use narrative principles of software
engineering such as behavioral design patterns during software development process.
So, the potential shortcomings and inconsistencies of the behavioral aspect of these
models are identified. This improves the process of gradual augmentation of design
decisions to the initial formal specification.
3
      </p>
    </sec>
    <sec id="sec-3">
      <title>The New Proposed Approach</title>
      <p>
        There has been an evolution in the way of transforming the models [
        <xref ref-type="bibr" rid="ref14">14</xref>
        ], [
        <xref ref-type="bibr" rid="ref21">21</xref>
        ], [
        <xref ref-type="bibr" rid="ref25">25</xref>
        ]. In
model transformation the most important issue is how to preserve the semantic and
the syntactic structure of model elements. To do so, this work will propose a
bidirectional meta-model-based transformation [
        <xref ref-type="bibr" rid="ref15">15</xref>
        ] between UML [
        <xref ref-type="bibr" rid="ref20">20</xref>
        ] and Object-Z
[
        <xref ref-type="bibr" rid="ref8">8</xref>
        ]. To do so, the two languages will be defined in terms of their meta-models. Then
these meta-models will be used to define a systematic transformation between the two
languages at the meta-level. In this way, we can provide a precise, consistent, and
complete transformation between the two languages. Such a transformation preserves
the semantics and the syntactic structure of models presented in both languages. Since
UML and Object-Z share basic object-oriented concepts, an attempt to create a
systematic transformation between the two languages seems sound. Proposing such a
meta-model-based mechanism is left for future work.
      </p>
      <p>
        As previously mentioned, we aim to visualize the behavioral aspect of formal
models of software to facilitate the possibility of using narrative techniques and
principles of software engineering during software development process to produce
reliable, yet flexible software. Design patterns are high level building blocks that
promote elegance in software by ordering proven and timeless solutions to common
problems in software design. Applying design patterns in software design has
important effects on software quality metrics such as flexibility, reusability,
scalability, and robustness [
        <xref ref-type="bibr" rid="ref11">11</xref>
        ], [
        <xref ref-type="bibr" rid="ref30">30</xref>
        ]. There are three types of design patterns,
including structural, creational, and behavioral patterns [
        <xref ref-type="bibr" rid="ref10">10</xref>
        ], [
        <xref ref-type="bibr" rid="ref11">11</xref>
        ]. According to the
goal of this work, we focus on the behavioral patterns which shift your focus away
from flow of control to let you concentrate just on the way objects are interconnected.
For more clarity, we analyze the software behavior from the view points of mediator,
observer, and state design patterns.
      </p>
      <p>Object-oriented design encourages the distribution of behavior among objects to
increase software reusability and flexibility. An important issue here is how peer
objects know about each other. Peers could maintain explicit references to each other,
but that would increase their coupling. Though distributing software into many
objects generally enhances reusability and flexibility, proliferating interconnections
tend to reduce reusability again. Moreover, it can be difficult to change the software
behavior in any significant way, since behavior is distributed among many objects.
Such a difficulty decreases the flexibility again. As a result, you may be forced to
define many subclasses to customize the software behavior. The mediator pattern
avoids this by introducing a mediator object between peers. Mediator promotes loose
coupling by keeping objects from referring to each other explicitly, and it lets you
vary their interaction independently. In this respect, we attempt to propose a
systematic approach to improve the quality of formal design from the viewpoint of the
mediator design pattern. That is, a formal design, in Object-Z, is received as an input,
and then behavior of this formal design is abstractly visualized, in UML, as an output.
Indeed, there is a focus on visualizing those aspects of the software behavior that are
prone to revising from the viewpoint of the mediator pattern. Moreover, this
approach, after full implementation, will automatically explore and recognize the
suitable times in order to review the software behavior from the view point of
mediator pattern throughout the software development process.</p>
      <p>Moreover, software distribution into a collection of cooperating classes requires
maintaining consistency among related objects. You don t want to achieve
consistency by making the classes tightly coupled, because that reduces their
reusability and flexibility. Observer pattern define a one-to-many dependency
between objects so that when one object changes state, all its dependents are notified
and updated automatically. In short, the required activities to visualizing the software
behavior (by focus on those aspects of behavior that are required for revision from the
viewpoint of observer pattern) include: 1) systematic elicitation of the objects that
their states are dependent on each other, 2) visualizing the discovered objects as
appropriate candidates for review, as well as 3) automatic proposing of the suitable
times to review the software behavior from the viewpoint of observer design pattern.</p>
      <p>We use the state design pattern in either of the following cases: 1) an object
behavior depends on its state, and its behavior must be changed at run-time depending
on its current state, 2) operations have large and multipart conditional statements that
depend on the object state. This state is usually represented by one or more
enumerated constants. Often, several operations will contain this same conditional
structure. The state pattern puts each branch of the conditional in a separate class.
This lets you treat the object state as an object in its own right that can vary
independently from other objects. State pattern allows an object to alter its behavior
when its internal state changes. The object will appear to change its class. Summarily,
the required activities to visualize the software behavior form the viewpoint of state
pattern include: 1) systematic discovery and elicitation of the objects that their
functions are dependent on their states, 2) visualizing the discovered objects as
appropriate candidates for review, as well as 3) automatic proposing of suitable times
for software behavior review from the viewpoint of the state design pattern.</p>
      <p>
        In all above-mentioned revision processes the required changes, revealed after
visualization, are re-formalized and thus the primary formal models are improved
from the view point of behavioral design patterns. Software behavior is visualized
from the required aspects using those UML diagrams that cover software behavior.
These diagrams include: 1) state diagram which illustrates the software behavior
through identifying the states and the events that result in changing the states [
        <xref ref-type="bibr" rid="ref23">23</xref>
        ],
[
        <xref ref-type="bibr" rid="ref24">24</xref>
        ], 2) activity diagram which visualizes the sequence, transposition, and
concurrence of the operations execution of the various functions at run-time, 3)
sequence diagram which represents the interactions among a set of objects and their
relationships [
        <xref ref-type="bibr" rid="ref23">23</xref>
        ].
      </p>
      <p>An appropriate evaluation method helps determine the overall effects or outcomes
of the new approach in relation to promised objectives. This method may indicate
whether the promised objectives were met, and also includes any recommendations
for improvement. As previously mentioned, the major goal of introducing the new
approach is to improve the process of formal modeling (including specification and
design) of software behavior based on visualization. So we should measure the
capability of the suggested approach in satisfying the expected goals. Evaluation
criteria of the proposed approach include: 1) correspondence percentage between
visual and formal models transformed to each other by the proposed meta-model
based transformation method, 2) the amount of increasing the quality (such as
flexibility, reusability, and scalability) of the developed system using the proposed
method.</p>
      <p>
        Case studies are one of the most common evaluation approaches in software
engineering [
        <xref ref-type="bibr" rid="ref8">8</xref>
        ], [
        <xref ref-type="bibr" rid="ref31">31</xref>
        ]. Based on this approach, the effectiveness and performance of
the new methods introduced by researches and studies are empirically measured from
the viewpoints of predefined evaluation criteria in one or more case studies. Besides,
in the mentioned case studies, the effectiveness and performance of new proposed
approaches are compared with existing related ones (if any). Indeed, another purpose
of defining the multi-lift system, addition the goal discussed in section 1, is to provide
a suitable test bed to empirically assess the new approach. Currently, the semi-formal
and formal specification of the multi-lift system is manually produced and presented
in Appendixes A and B. As previously mentioned, proposing the new approach in
integrating the UML and Object-Z is left for future work. After that, the new approach
will be applied on the formal specification that is manually produced. Then the output
will be compared with the existing semi-formal specification. The more these two
models are similar, the more the new approach will be precise. So by performing this
experiment, we will empirically demonstrate the correctness of the proposed approach
as well as the amount of increasing the flexibility of the developed system. Moreover,
as mentioned before, we intend to propose a meta-model-based transformation
approach. So we will define a formal and systematic transformation between the two
languages at the meta-level. In this way, we can prove the correctness, precision, and
completeness of the transformation process mathematically. There are also some
attempts to measuring software flexibility rather than case studies [
        <xref ref-type="bibr" rid="ref32">32</xref>
        ].
4
      </p>
    </sec>
    <sec id="sec-4">
      <title>Conclusion and Future Works</title>
      <p>The widespread use of semi-formal methods in mainstream software development
leads to highly flexible software. However, they do not take a precise approach to
software development in domains where reliability is absolutely crucial, such as
safety-critical and high integrity systems. Their semantics are not well defined.
Formal methods offer the ability to specify and verify software using mathematical
logic. They have precise semantics, allowing for less ambiguous models of systems to
be designed. However their use has not been widely adopted due to the mathematical
nature of the languages.</p>
      <p>This work proposes a new approach to integrate visual and formal models to
exploit their advantages in producing reliable, yet flexible software. To do so, this
work intends to present a meta-model-based transformation between UML and
Object-Z. These two languages will be defined in terms of their meta-models, and a
systematic transformation between the models will be provided at the meta-level. As a
result, we can provide a precise, consistent, and complete transformation between a
visual model in UML and a formal model in Object-Z. Visualizing the formal models
prepares an appropriate ground to revise them from the viewpoints of design patterns
which in turn leads to produce high quality software. In the multi-lift case study, we
will illustrate how the meta-model-based transformation enables us to create a UML
visual representation of an Object-Z specification and vice versa. Although, this paper
draws the path towards solving the defined problem and achieving the promised
goals, proposing the meta-model-based transformation is left for future work.</p>
      <p>
        Integrated methods research has taught us many things: (a) visual modeling
notations and formal methods can coexist within the same development and
complement each other when developing software models, (b) this coexistence is
useful and provides many benefits, and (c) formalization of diagrammatic languages,
like UML, and visualization of formal models, like Object-Z, is far from trivial.
Integrated methods, like formal methods, never really caught-on. A detailed study is
given in [
        <xref ref-type="bibr" rid="ref1">1</xref>
        ]. The works that have already been done are just a step in the right
direction, but much more is yet to be done. The most frequently adopted approach is
to define transformations between the visual and formal models [
        <xref ref-type="bibr" rid="ref1">1</xref>
        ], [
        <xref ref-type="bibr" rid="ref2">2</xref>
        ], [
        <xref ref-type="bibr" rid="ref5">5</xref>
        ], [
        <xref ref-type="bibr" rid="ref8">8</xref>
        ], [
        <xref ref-type="bibr" rid="ref12">12</xref>
        ],
[
        <xref ref-type="bibr" rid="ref22">22</xref>
        ]. However, a significant problem with these suggested approaches is that the
transformation itself is often described imprecisely, with the result that the overall
transformation task may be imprecise and incomplete. Consequently, the confidence
the developer may have in the models is reduced, making the transformation approach
unreliable.
      </p>
      <p>
        There are several attempts to formalize the UML [
        <xref ref-type="bibr" rid="ref15">15</xref>
        ], [
        <xref ref-type="bibr" rid="ref18">18</xref>
        ], [
        <xref ref-type="bibr" rid="ref26">26</xref>
        ], [
        <xref ref-type="bibr" rid="ref28">28</xref>
        ], [
        <xref ref-type="bibr" rid="ref31">31</xref>
        ], [
        <xref ref-type="bibr" rid="ref33">33</xref>
        ].
None of them achieves a full UML formalization. Instead, they focus on a restricted
subset of the language, mostly class and state diagrams. Most approaches do not even
attempt to formalize all features of a diagram, focusing on those features that are
appropriate for the purpose of the approach. Despite some improvements, the
integrations that have been proposed are still not practical, which limits their
engineering value. Moreover, the integration still falls behind the vision of very
specialized software engineering methods. There are also several attempts to integrate
design patterns into mainstream software development process [
        <xref ref-type="bibr" rid="ref11">11</xref>
        ] as well as to
formalize design patterns [
        <xref ref-type="bibr" rid="ref4">4</xref>
        ], [
        <xref ref-type="bibr" rid="ref9">9</xref>
        ], [
        <xref ref-type="bibr" rid="ref15 ref16">15-16</xref>
        ]. Generally, despite some improvements in
integrating patterns and formalism, the approaches that describe patterns formally are
limited in their expressibility and reuse mechanisms.
      </p>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          1. Am?lio, N.:
          <article-title>Generative frameworks for rigorous model-driven development</article-title>
          .
          <source>PhD thesis</source>
          , Dept. of Computer Science, University of York (
          <year>2006</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          2.
          <string-name>
            <surname>Anastasakis</surname>
            ,
            <given-names>K.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Bordbar</surname>
            ,
            <given-names>B.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Georg</surname>
            ,
            <given-names>G.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Ray</surname>
            ,
            <given-names>I.</given-names>
          </string-name>
          :
          <article-title>UML2Alloy: A Challenging Model Transformation</article-title>
          .
          <source>In: ACM/IEEE 10th International Conference on Model Driven Engineering Languages and Systems (MoDELS)</source>
          , pp.
          <fpage>436</fpage>
          --
          <lpage>450</lpage>
          (
          <year>2007</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          3. Bj?rner, D.: Software Engineering 3: Domains, Requirements, and Software Design. Springer (
          <year>2006</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          4.
          <string-name>
            <surname>Blazy</surname>
            ,
            <given-names>S.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Gervais</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Laleau</surname>
          </string-name>
          , R.:
          <article-title>Reuse of specification patterns with the B method</article-title>
          .
          <source>In: ZB</source>
          <year>2003</year>
          , Turku, Finland,
          <string-name>
            <surname>LNCS</surname>
          </string-name>
          , vol.
          <volume>2651</volume>
          , Springer, pp.
          <fpage>40</fpage>
          --
          <lpage>57</lpage>
          (
          <year>2003</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          5.
          <string-name>
            <surname>Bouquet</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Dadeau</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Groslambert</surname>
          </string-name>
          , J.:
          <article-title>Checking JML specifications with B machines</article-title>
          .
          <source>In: ZB</source>
          <year>2005</year>
          ,
          <article-title>LNCS</article-title>
          , vol.
          <volume>3455</volume>
          , Springer, pp.
          <fpage>434</fpage>
          --
          <lpage>453</lpage>
          (
          <year>2005</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref6">
        <mixed-citation>
          6.
          <string-name>
            <surname>Charatan</surname>
            ,
            <given-names>Q.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Kans</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          :
          <article-title>Formal Software Development: From VDM to Java</article-title>
          . Palgrave
          <string-name>
            <surname>Macmillan</surname>
          </string-name>
          (
          <year>2004</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref7">
        <mixed-citation>
          7.
          <string-name>
            <surname>Charette</surname>
            ,
            <given-names>R.N.</given-names>
          </string-name>
          :
          <article-title>Why software fails</article-title>
          ,
          <source>IEEE Spectrum</source>
          . vol.
          <volume>42</volume>
          (
          <issue>9</issue>
          ), pp.
          <fpage>42</fpage>
          --
          <lpage>49</lpage>
          (
          <year>2005</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref8">
        <mixed-citation>
          8.
          <string-name>
            <surname>Duke</surname>
            ,
            <given-names>R.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Rose</surname>
            ,
            <given-names>G.: Formal</given-names>
          </string-name>
          <string-name>
            <surname>Object-Oriented Specification Using Object-Z. MacMillan Press</surname>
          </string-name>
          (
          <year>2000</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref9">
        <mixed-citation>
          9.
          <string-name>
            <surname>Flores</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Moore</surname>
            ,
            <given-names>R.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Reynoso</surname>
            ,
            <given-names>L.</given-names>
          </string-name>
          :
          <article-title>A formal model of object-oriented design and GoF design patterns</article-title>
          .
          <source>In: FME</source>
          <year>2001</year>
          ,
          <article-title>LNCS</article-title>
          , vol.
          <year>2021</year>
          , pp.
          <fpage>223</fpage>
          --
          <lpage>241</lpage>
          , Springer (
          <year>2001</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref10">
        <mixed-citation>
          10.
          <string-name>
            <surname>Freeman</surname>
            ,
            <given-names>E.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Freeman</surname>
            ,
            <given-names>E.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Kathy Sierra</surname>
            ,
            <given-names>B.: Head</given-names>
          </string-name>
          <string-name>
            <surname>First Design Patterns. O Reilly Media</surname>
          </string-name>
          ,
          <article-title>First edition (</article-title>
          <year>2004</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref11">
        <mixed-citation>
          11.
          <string-name>
            <surname>Gamma</surname>
            ,
            <given-names>E.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Helm</surname>
            ,
            <given-names>R.</given-names>
          </string-name>
          , Johnson, R.,
          <string-name>
            <surname>Vlissides</surname>
          </string-name>
          , J.: Design Pattern:
          <article-title>Elements of Reusable Object-Oriented Software</article-title>
          . Addison-Wesley Publishing Company, Fifth printing (
          <year>1995</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref12">
        <mixed-citation>
          12.
          <string-name>
            <surname>Jackson</surname>
            ,
            <given-names>D.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Schechter</surname>
            ,
            <given-names>I.</given-names>
          </string-name>
          , and
          <string-name>
            <surname>Shlyakhter</surname>
          </string-name>
          , I.:
          <article-title>Alcoa: the Alloy constraint analyzer</article-title>
          .
          <source>In: International Conference on Software Engineering</source>
          , Limerick, Ireland, pp.
          <fpage>730</fpage>
          <lpage>733</lpage>
          (
          <year>2000</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref13">
        <mixed-citation>
          13.
          <string-name>
            <surname>Jackson</surname>
            ,
            <given-names>D.</given-names>
          </string-name>
          :
          <article-title>Software Abstractions: logic, language and analysis</article-title>
          . MIT Press (
          <year>2006</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref14">
        <mixed-citation>
          14.
          <string-name>
            <surname>Kessentini</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Wimmer</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Sahraoui</surname>
            ,
            <given-names>H.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Boukadoum</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          :
          <article-title>Generating Transformation Rules from Examples for Behavioral Models</article-title>
          . In: Second International Workshop on Behavior Modeling: Foundation and Applications, Paris, France (
          <year>2010</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref15">
        <mixed-citation>
          15.
          <string-name>
            <surname>Kim</surname>
            ,
            <given-names>S.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Carrington</surname>
            ,
            <given-names>D.:</given-names>
          </string-name>
          <article-title>A formal meta-modeling approach to a transformation between the UML state machine and Object-Z</article-title>
          .
          <source>In: ICFEM</source>
          <year>2002</year>
          ,
          <article-title>LNCS</article-title>
          , vol.
          <volume>2495</volume>
          , Springer, pp.
          <fpage>548</fpage>
          --
          <lpage>560</lpage>
          (
          <year>2002</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref16">
        <mixed-citation>
          16.
          <string-name>
            <surname>Kim</surname>
            ,
            <given-names>S.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Carrington</surname>
            ,
            <given-names>D.:</given-names>
          </string-name>
          <article-title>A rigorous foundation for pattern-based design models</article-title>
          .
          <source>In: ZB</source>
          <year>2005</year>
          ,
          <article-title>LNCS</article-title>
          , vol.
          <volume>3455</volume>
          , Springer, pp.
          <fpage>242</fpage>
          --
          <lpage>261</lpage>
          (
          <year>2005</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref17">
        <mixed-citation>
          17.
          <string-name>
            <surname>Liang</surname>
            ,
            <given-names>H.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Song</surname>
            <given-names>Dong</given-names>
          </string-name>
          ,
          <string-name>
            <given-names>J.</given-names>
            ,
            <surname>Sun</surname>
          </string-name>
          ,
          <string-name>
            <given-names>J.</given-names>
            ,
            <surname>Wong</surname>
          </string-name>
          ,
          <string-name>
            <surname>W.</surname>
          </string-name>
          :
          <article-title>Software monitoring through formal specification animation</article-title>
          .
          <source>J. of Innovations in Systems and Software Eng.</source>
          , vol.
          <volume>5</volume>
          (
          <issue>4</issue>
          ), pp.
          <fpage>231</fpage>
          --
          <lpage>241</lpage>
          (
          <year>2009</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref18">
        <mixed-citation>
          18.
          <string-name>
            <surname>Miao</surname>
            ,
            <given-names>H.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Liu</surname>
            ,
            <given-names>L.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Li</surname>
            ,
            <given-names>L.</given-names>
          </string-name>
          :
          <article-title>Formalizing UML models with Object-Z</article-title>
          . In: ICFEM2002, Springer-Verlag, pp.
          <fpage>523</fpage>
          --
          <lpage>534</lpage>
          (
          <year>2002</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref19">
        <mixed-citation>
          19.
          <article-title>The economic impacts of inadequate infrastructure for software testing</article-title>
          .
          <source>Technical report, National Institute of Standards and Technology (NIST)</source>
          ,
          <year>2002</year>
          , http://www.nist.gov/
        </mixed-citation>
      </ref>
      <ref id="ref20">
        <mixed-citation>
          20.OMG,
          <article-title>Object Constraint Language (OCL)</article-title>
          .
          <source>version 2</source>
          .0, Object Management Group, http://www.uml.org/ (
          <year>2006</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref21">
        <mixed-citation>
          21.
          <string-name>
            <surname>Poernomo</surname>
            ,
            <given-names>I.</given-names>
          </string-name>
          :
          <article-title>Proofs-as-model-transformations</article-title>
          .
          <source>LNCS</source>
          , vol.
          <volume>5063</volume>
          , pp.
          <fpage>214</fpage>
          --
          <lpage>228</lpage>
          (
          <year>2008</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref22">
        <mixed-citation>
          22.
          <string-name>
            <surname>Polack</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          :
          <article-title>SAZ: SSADM version 4</article-title>
          and
          <string-name>
            <surname>Z.</surname>
          </string-name>
          <article-title>In: Software Specification Methods: an overview using a case study</article-title>
          .
          <source>FACIT</source>
          , Springer, pp.
          <fpage>21</fpage>
          --
          <lpage>38</lpage>
          (
          <year>2001</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref23">
        <mixed-citation>
          23.
          <string-name>
            <surname>Porres</surname>
            ,
            <given-names>I.</given-names>
          </string-name>
          :
          <article-title>Modeling and Analyzing Software Behavior in UML</article-title>
          .
          <source>PhD thesis</source>
          , Department of Computer Science, Abo Akademi University, Finland (
          <year>2001</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref24">
        <mixed-citation>
          24.
          <string-name>
            <surname>Pressman</surname>
          </string-name>
          , R.:
          <source>Software Engineering: A Practitioner s Approach. 7th edition</source>
          ,
          <source>McGraw Hill</source>
          (
          <year>2009</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref25">
        <mixed-citation>
          25.
          <string-name>
            <surname>Rahimi</surname>
            ,
            <given-names>S.K.</given-names>
          </string-name>
          :
          <article-title>Specification of UML Model Transformations</article-title>
          .
          <source>In: Third International Conference on Software Testing, Verification and Validation</source>
          , pp.
          <fpage>323</fpage>
          --
          <lpage>326</lpage>
          , Paris (
          <year>2010</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref26">
        <mixed-citation>
          26.
          <string-name>
            <surname>Razali</surname>
            ,
            <given-names>R.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Snook</surname>
            ,
            <given-names>C.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Poppleton</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Garratt</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          :
          <article-title>Usability Assessment of a UML-based Formal Modeling Method Using Cognitive Dimensions Framework</article-title>
          .
          <source>Human Technology: An Interdisciplinary J. on Humans in ICT Environments</source>
          (
          <year>2008</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref27">
        <mixed-citation>
          27.
          <string-name>
            <surname>Schmidt</surname>
            ,
            <given-names>D.C.</given-names>
          </string-name>
          :
          <article-title>Model-driven engineering</article-title>
          . IEEE Computer,
          <volume>39</volume>
          (
          <issue>2</issue>
          ), pp.
          <fpage>25</fpage>
          --
          <lpage>31</lpage>
          (
          <year>2006</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref28">
        <mixed-citation>
          28.
          <string-name>
            <surname>Snook</surname>
            ,
            <given-names>C.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Butler</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          :
          <string-name>
            <surname>UML-B</surname>
          </string-name>
          :
          <article-title>Formal modeling and design aided by UML</article-title>
          .
          <source>ACM Trans. Softw. Eng. Methodol</source>
          , vol.
          <volume>15</volume>
          (
          <issue>1</issue>
          ), pp.
          <fpage>92</fpage>
          --
          <lpage>122</lpage>
          (
          <year>2006</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref29">
        <mixed-citation>
          29.
          <string-name>
            <surname>Sommerville</surname>
            ,
            <given-names>I.</given-names>
          </string-name>
          :
          <source>Software Engineering. 8th edition</source>
          ,
          <source>Addison Wesley, June</source>
          <volume>4</volume>
          (
          <year>2006</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref30">
        <mixed-citation>
          30.
          <string-name>
            <surname>Stepney</surname>
            ,
            <given-names>S.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Polack</surname>
            ,
            <given-names>F.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Toyn</surname>
            ,
            <given-names>I.</given-names>
          </string-name>
          :
          <article-title>Patterns to guide practical refactoring: examples targeting promotion in Z</article-title>
          .
          <source>In: ZB</source>
          <year>2003</year>
          ,
          <article-title>Finland</article-title>
          ,
          <string-name>
            <surname>LNCS</surname>
          </string-name>
          , vol.
          <volume>2651</volume>
          of, Springer, pp.
          <fpage>20</fpage>
          --
          <lpage>39</lpage>
          (
          <year>2003</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref31">
        <mixed-citation>
          31.
          <string-name>
            <surname>Williams</surname>
            ,
            <given-names>J.R.</given-names>
          </string-name>
          :
          <article-title>Automatic Formalization of UML to Z</article-title>
          .
          <source>MSc Thesis</source>
          , Department of Computer Science, University of York (
          <year>2009</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref32">
        <mixed-citation>
          32.
          <string-name>
            <surname>Eden</surname>
            ,
            <given-names>A.H.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Mens</surname>
            ,
            <given-names>T.</given-names>
          </string-name>
          :
          <article-title>Measuring Software Flexibility</article-title>
          .
          <source>IEE Software</source>
          , vol.
          <volume>153</volume>
          (
          <issue>3</issue>
          ), pp.
          <fpage>113</fpage>
          --
          <lpage>126</lpage>
          . London, UK:
          <article-title>The Institution of Engineering and Technology (</article-title>
          <year>2006</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref33">
        <mixed-citation>
          33.
          <string-name>
            <surname>Evans</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          , France,
          <string-name>
            <given-names>R.</given-names>
            ,
            <surname>Lano</surname>
          </string-name>
          ,
          <string-name>
            <given-names>K.</given-names>
            ,
            <surname>Rumpe</surname>
          </string-name>
          ,
          <string-name>
            <surname>B.</surname>
          </string-name>
          :
          <article-title>The UML as a Formal Modeling Notation</article-title>
          .
          <source>In UML'98: Beyond the Notation</source>
          , Mulhouse, France, vol.
          <volume>1618</volume>
          , LNCS, Springer, pp.
          <fpage>336</fpage>
          -
          <lpage>348</lpage>
          (
          <year>1998</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref34">
        <mixed-citation>
          34.
          <string-name>
            <surname>Rasoolzadegan</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Abdollahzadeh</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          :
          <article-title>Empirical Evaluation of Modeling Languages Using Multi-Lift System Case Study</article-title>
          .
          <source>In MSV'11: The 8th annual International Conference on Modeling, Simulation and Visualization Methods</source>
          , Las Vegas, Nevada, USA (
          <year>2011</year>
          )
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>