@MASTERSTHESIS\{IMM2003-02856,
    author       = "C. K. Madsen",
    title        = "Integration of Specification Techniques",
    year         = "2003",
    keywords     = "Specification methods, {RAISE} Specication Language, graphical specification techniques, Live Sequence Charts, Statecharts.",
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    note         = "Advisor: Dines Bj{\o}rner",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/2856-full.html",
    abstract     = "Graphical specification notations have gained much popularity in software engineering, as witnessed by the widespread adoption of {UML} throughout the software industry. Graphical notations are generally characterised by being intuitive to understand, i.e. new users of these notation require little training to become familiar with them. However, few of the graphical notations have a formally defined meaning, so diagrams expressed in such notations are ambiguous - a highly undesirable property for a specification notation. In contrast, formal specification languages have a formally defined mathematical meaning but are comprehensible only to properly educated software engineers. The implication of this is that specifications developed using formal languages are not immediately understandable to the customers and domain experts, and therefore they are difficult to validate. In this thesis we describe the graphical notations of Live Sequence Charts and Statecharts and propose a method using diagrams in these notations for constraining a formal speci cation expressed in a subset of the {RAISE} Specification Language. Furthermore, we propose a development method that combines the traditional approach with that of formal development. We give a small example illustrating the application of this method.

In Danish:

Grafiske specifikationsnotationer har opn{\aa}et stor popularitet indenfor softwareudvikling, hvilket blandt andet ses i den store udbredelse af {UML} i softwareindustrien. Grafiske notationer er generelt set karakteriseret ved at v{\ae}re intuitive at forst{\aa}, det vil sige at nye brugere af disse notationer har kun behov for kortvarig tr{\ae}ning for at bliver fortrolige med dem. Desv{\ae}rre er det kun f{\aa} grafiske notationer, som har en formelt matematisk defineret betydning. Derfor vil diagrammer udtrykt i s{\aa}danne notationer som oftest v{\ae}re tvetydige, hvilket er en uhensigtsm{\ae}ssig egenskab ved en notation beregnet til specifikation. Mods{\ae}tningen er formelle specfikationssprog, der har en pr{\ae}cis matematisk defineret betydning, men som kun er forst{\aa}elige for veluddannede softwareudviklere. Resultatet er, at specifikationer udarbejdet ved brug af formelle notationer ikke umiddelbart kan forst{\aa}s af kunder og eksperter i dom{\ae}net, hvilket medf{\o}rer at disse specifikationer er sv{\ae}re at validere. I denne afhandling beskriver vi de to grafiske notationer Live Sequence Charts og Statecharts og foresl{\aa}r en metode, der bruger diagrammer udtrykt i disse notationer til at opstille betingelser som skal opfyldes af en formel specifikation skrevet i et uddrag af sproget {RAISE} Specification Language. Desuden foresl{\aa}s en udviklingsmetode, som kombinerer den traditionelle metode med den model, der bruges indenfor formel softwareudvikling. Metoden illustreres med et mindre eksempel p{\aa} dens anvendelse."
}