Information Technology Reference
In-Depth Information
consistency:
Administration
||
Machine
||
Researcher
Adding a component
consistency:
Administration
||
Machine
Fig. 5.
OnepossiblestepinBottom-updevelopment:Checkingconsistencybeforeand
afteraddinganextracomponent
||
||
UniSpec
Machine
Researcher
Administration
≤
Factoring out some behaviour
||
UniSpec
Machine
Researcher
≤
\\
Administration
Fig. 6.
One possible step in Stepwise modularisation of requirements: Factoring out
thebehaviouroftheAdministration
thatmodelsaremadethatdescribethebehaviourofthesecomponents.Theaim
ofthebottom-updevelopmentinoursettingistoverifythatacompletesystem
canbebuiltfromthepreexistingcomponents.Figure5showsonepossiblestepin
abottom-updevelopmentprocess.Hereaconsistencycheckisperformedonthe
parallelcompositionoftwocomponentsafterwhichanothercomponentisadded
andtheconsistencycheckisredone.Thebottomupdevelopmentmethodology
could easily be combined with refinement checking where the overall require-
ments are stepwise refined to see what the actual combination of components
canguaranteeintermsofbehaviourandtiming.
Stepwise Modularisation of Requirements.
The third and more novel type of
development methodologythat our frameworksupports is the
Stepwise modu-
larisation of requirements
. Here the idea is, like for the
top-down development
tostartwithageneralspecificationoftherequirementstothesystemandthen
usingthe
quotient
operatortofactoroutbehaviourthatisalreadyimplemented
byexistingcomponents,sothatoneisleftwithaspecificationforthemissingbe-
haviour.Thisspecification,whichissynthesisedbythetool,cannowbefurther
refinedto providetheimplementationofmissingfunctionalityintermsofnew
components.Inthatthisprocessgeneralisesstepwiserefinementandbottom-up
synthesis. Figure 6 shows how one component can be moved from one side of
therefinementchecktotheotherbyfactoringoutthebehaviour.
Anotheraspectofourframeworkthatcanbeusedorthogonallytothethree
described development ideas is conjunction. Conjunction allows to specify dif-
ferent aspects or requirements to a component and then compose these using
logical conjunction, such that an implementation would have to individually
satisfy each conjunct in order to satisfy the conjunction. Figure 7 shows an
exampleoftwospecificationsthateachhandleoneaspectoftheresponsibilities
