Several studies have been conducted on formal methods; however, few of these studies
have used formal methods in the data warehousing area, specifically system
development. Many reasons may be linked to that, such as that few experts know how to
use them. Formal methods have been used in software development using mathematical
notations. Despite the advantages of using formal methods in software development,
their application in the data warehousing area has been restricted when compared with
the use of informal (natural language) and semi-formal notations.
This research aims to determine the extent to which formal methods may mitigate failures
that mostly occur in the development of data warehouse systems. As part of this research,
an enhanced framework was proposed to facilitate the usage of formal methods in the
development of such systems. The enhanced framework focuses mainly on the
requirements definition, the Unified Modelling Language (UML) constructs, the Star
model and formal specification. A medium-sized case study of a data mart was
considered to validate the enhanced framework. This dissertation also discusses the
object-orientation paradigm and UML notations.
The requirements specification of a data warehouse system is presented in natural
language and formal notation to show how a formal specification may be drifted from
natural language to UML structures and thereafter to the Z specification using an
established strategy as a guideline to construct a Z specification
Alhoewel verskeie studies oor formele metodes gedoen is, het min hiervan formele
metodes in die databergingarea, spesifiek stelselontwerp, gebruik. Dit kan aan baie redes
toegeskryf word, soos dat min kundiges weet hoe om dit te gebruik. Formele metodes is
in sagtewareontwikkeling gebruik wat wiskundige notasies gebruik. Ten spyte van die
voordele van formele metodes in sagtewareontwikkeling, is die toepassing daarvan in
die databergingarea beperk wanneer dit met die gebruik van informele (natuurlike taal)
en semiformele notasies vergelyk word.
Hierdie navorsing beoog om te bepaal tot watter mate formele metodes foute kan
uitskakel wat hoofsaaklik in die ontwikkeling van databeringstelsels voorkom. As deel
van hierdie navorsing is 'n beter raamwerk voorgestel om die gebruik van formele
metodes in die ontwikkeling van sulke stelsels te fasiliteer. Die beter raamwerk fokus
hoofsaaklik op die definisie van vereistes, die Unified Modelling Language (UML) -
konstukte, die Star-model en formele spesifikasies. Die mediumgrootte gevallestudie van
'n datamark is oorweeg om die beter raamwerk geldig te verklaar. Hierdie verhandeling
bespreek ook die voorwerpgeoriënteerde paradigma en die UML-notasies.
Die vereiste spesifikasie van 'n databergingstelsel word in natuurlike taal en formele
notasie voorgehou om aan te dui hoe 'n formele spesifikasie van natuurlik taal na UML strukture kan verskuif en daarna na die Z-spesifiekasie deur 'n gevestigde strategie as 'n
riglyn te gebruik om 'n Z-spesifikasie te konstrueer.
Go nnile le dithutopatlisiso di le mmalwa ka mekgwa e e fomale, fela ga se
dithutopatlisiso tse dintsi tsa tseno tse di dirisitseng mekgwa e e fomale mo karolong ya
bobolokelobogolo jwa data, bogolo segolo mo ntlheng ya thadiso ya ditsamaiso tsa
dikhomphiutha. Go ka nna le mabaka a le mantsi a a ka golaganngwang le seno, go
tshwana le gore ga se baitseanape ba le kalo ba ba itseng go e dirisa. Mekgwa e e fomale
e e dirisitswe mo tlhabololong ya dirweboleta go dirisiwa matshwao a dipalo. Le fa go
na le melemo ya go dirisa mekgwa e e fomale mo tlhabololong ya dirweboleta, tiriso ya
yona mo bobolokelobogolong jwa data e lekanyeditswe fa e tshwantshanngwa le tiriso ya
matshwao a a seng fomale (puo ya tlwaelo) le a a batlang a le fomale.
Patlisiso eno e ikaelela go bona gore a mekgwa e e fomale e ka fokotsa go retelelwa go go
diragalang gantsi mo tlhabololong ya ditsamaiso tsa bobolokelobogolo jwa data. Jaaka
karolo ya patlisiso eno, go tshitshintswe letlhomeso le le tokafaditsweng go bebofatsa
tiriso ya mekgwa e e fomale mo tlhabololong ya ditsamaiso tse di jalo. Letlhomeso le le
tokafaditsweng le tota ditlhokego tsa tlhaloso, megopolo ya Unified Modelling Language
(UML), sekao sa Star le ditlhokego tse di rulaganeng. Go dirisitswe patlisiso ya tobiso e e
magareng ya data mart go tlhomamisa letlhomeso le le tokafaditsweng. Tlhotlhomisi eno
gape e lebelela pharataeme e e totileng sedirwa/selo le matshwao a UML.
Ditlhokego tsa tsamaiso ya polokelokgolo ya data di tlhagisiwa ka puo ya tlholego le matshwao a a fomale go bontsha ka moo tlhagiso e e fomale e ka lebisiwang go tswa kwa
puong ya tlholego go ya kwa dipopegong tsa UML mme morago e lebe kwa tlhalosong
ya ditlhokego ya Z go dirisiwa togamaano e e ntseng e le gona jaaka kaedi ya go aga
tlhaloso ya ditlhokego ya Z.
