Beta 1


Title Integration of Specification Techniques
Author Madsen, Christian Krog
Supervisor Bjørner, Dines (Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Master's thesis
Year 2003
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å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ære intuitive at forstå, det vil sige at nye brugere af disse notationer har kun behov for kortvarig træning for at bliver fortrolige med dem. Desværre er det kun få grafiske notationer, som har en formelt matematisk defineret betydning. Derfor vil diagrammer udtrykt i sådanne notationer som oftest være tvetydige, hvilket er en uhensigtsmæssig egenskab ved en notation beregnet til specifikation. Modsætningen er formelle specfikationssprog, der har en præcis matematisk defineret betydning, men som kun er forståelige for veluddannede softwareudviklere. Resultatet er, at specifikationer udarbejdet ved brug af formelle notationer ikke umiddelbart kan forstås af kunder og eksperter i domænet, hvilket medfører at disse specifikationer er svære at validere. I denne afhandling beskriver vi de to grafiske notationer Live Sequence Charts og Statecharts og foreslå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ås en udviklingsmetode, som kombinerer den traditionelle metode med den model, der bruges indenfor formel softwareudvikling. Metoden illustreres med et mindre eksempel på dens anvendelse.
Imprint Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU : DK-2800 Kgs. Lyngby, Denmark
Keywords Specification methods; RAISE Specication Language; graphical specification techniques; Live Sequence Charts; Statecharts.
Fulltext
Original PDF imm2856.pdf (0.57 MB)
Admin Creation date: 2006-06-22    Update date: 2012-12-20    Source: dtu    ID: 58639    Original MXD