So wa e P ocess Modelling as Rela ionships be ween Tasks
Xa ie F anch
[email p o ec ed]
Uni e si a Poli kcnica de Ca alunya
Jo di Gi ona 1-3,08034 Ba celona
Ca alonia (Spain)
FAX: 34-3-4017014. Phone: 34-3-4016965
Abs ac
Sys ema ic o mula ion
o
so wa e p ocess models is
cu en ly a challenging p oblem in so wa e enginee ing.
We p esen he e an app oach o de ine models co e ing he
phases o speci ica ion, design, implemen a ion and
es ing o so wa e sys ems in he componen
p og amming amewo k, aking in o accoun
non- unc ional aspec s o so wa e (e iciency, e c.},
au oma ic eusabili y o implemen a ions in sys ems and
also p o o yping echniques in ol ing bo h speci ica ions
and implemen a ions. Ou p oposal elies
on
he
iden i ica ion o a ca alogue o asks ha appea du ing
hese phases which sa is y some ela ionships conce ning
hei o de o execu ion.
A
so wa e p ocess model can be
de ined as he addi ion
o
mo e ela ionships o e hese
asks using a simple, modula p ocess language. We ha e
de eloped also a o mal de ini ion o co ec ness o a
sojiwa e de elopmen wi h espec o a so wa e p ocess
model, based
on
he o mula ion o models as g aphs.
1.
In oduc ion
I is widely ecognised ha one
o
he mos challenging
p oblems in he ield o so wa e enginee ing
is
he
sys ema ic o mula ion o so wa e p ocess models in a
such a way ha i can be said ha so wa e p ocesses a e
so wa e oo [13].
A
lo o esea ch has been done in his
ield and, as a esul , some p oposals ha e been de ined,
which can be cha ac e ised by he kind o language o
o malism used o ep esen he model: impe a i e
p og ams
[
18, 21, ans o ma ion ules o e speci ica ions
and p og ams
[
121, composi ion o in e ence ules
[
141,
mul i iew app oaches [17] and
so
on; [7] gi es a
p esen a ion
o
many p ojec s ecen ly de eloped
(including exhaus i e e e ence lis s). Some me hods
add ess o he whole so wa e p ocess, while o he s ocus
on a subse o phases o he li e-cycle (usually,
speci ica ion and design); anyway, he exis ence o hose
p oposals is a s ep beyond he uni o m ea men o
1089-6503197 $10.00
0
1997
IEEE
199
Josep
M.
Rib6
j osepma
@
eup.udl .es
Uni e si a de Lleida
P. Vic o Siu ana 1,25003 Lleida
Ca alonia (Spain)
FAX: 34-73-702 162. Phone: 34-73-702000
p oduc s (so wa e) and p ocesses (de elopmen s) in
so wa e enginee ing, as we hink i should be.
In his pape , we a e going o p esen a amewo k o
o mula e so wa e p ocess models o componen
p og amming [lo, 151, assigning a p ominen ole o he
managemen o ope a ional aspec s o so wa e (as
e iciency o eliabili y); we also emphasise p o o yping
and eusabili y o (implemen a ion
o )
componen s. Mo e
p ecisely, we conside a subse o he whole so wa e
p ocess composed by speci ica ion, design,
implemen a ion and es ing phases, and we iden i y a
ca alogue o asks ha a ise du ing hese ac i i ies, s a ing
some p ecedence ela ionships be ween hem. We de ine
hen a p ocess language cha ac e ised by he s a emen o
new ela ionships be ween asks; he language has been
designed wi h he goal o simplici y and modula i y in
mind and,
so,
i seems o be easy o lea n and use.
Also,
we p o ide a o mal de ini ion o he concep o
co ec ness o
a
so wa e de elopmen wi h espec o a
p ocess model de ined wi h his language.
2.
The amewo k
We a e in e es ed in so wa e sys ems as a hie a chy o
so wa e componen s.
A
componen
is
de ined by means
o a speci ica ion, which includes wo pa s: he unc ional
one, s a ing how does he componen beha e, and he
non- unc ional one, ha decla es addi ional equi emen s
e e ed o some ope a ional a ibu es (as e iciency); hese
a ibu es a e de ined in p ope y modules, impo ed in
non- unc ional speci ica ions. Once he speci ica ion is
comple e, many implemen a ions may be buil o his
componen , all o hem sa is ying he p ope ies s a ed in
bo h pa s o he speci ica ion; implemen a ions include a
desc ip ion o hei non- unc ional beha iou , which
de e mines he alues ha he ope a ional a ibu es
decla ed in he non- unc ional speci ica ion ake in he
implemen a ion, possibly s a ing some addi ional
cons ains on implemen a ions
o
impo ed componen s.
Up o now, ou me hod has been de ined o e an
ad hoc
language called
Me li.
Me li includes ea u es o build
unc ional and non- unc ional speci ica ions and
implemen a ions. The eason o wo king wi h Me li is
wo old. On he one hand, i will be no necessa y o
de elop new ools when conside ing conc e e speci ica ion
and implemen a ion languages, excep om a ansla o
om hem o Me li. On he o he hand, we ha e de ined an
execu ion ool o e Me li
[l]
able o p o o ype sys ems
ha combine speci ica ions and p og ams p o ided ha
some condi ions hold. Howe e , i mus emain clea ha
he me hodology we a e going o p opose does no depend
o he languages used o speci y componen s and o
implemen hem (p o ided ha hey ha e simila
cha ac e is ics o he ones adop ed in Me li);
so,
we a e no
equi ing o lea n Me li o adop ou p oposal.
A mo e de ailed desc ip ion o Me li may be ound a
[4,
61; we gi e he e jus he highligh s o unde s and he
amewo k o ou p oposal.
2.1.
Func ional speci ica ions
We conside wo kinds o unc ional speci ica ions:
Model-o ien ed speci ica ions. As in
Z
[16] o VDM
[
1
11,
whe e a model o he componen is s a ed and he
speci ica ion is exp essed mainly by means o p e and
pos condi ions o e he model.
Algeb aic speci ica ions.
As
in La ch
[8]
o
OBJ3
[9],
he speci ica ion consis s o a se o equa ions. We a e
pa icula ly in e es ed in he possibili y o using
di e en seman ics (ini ial and beha iou al, as La ch
does) o in e p e he equa ions.
2.2.
Non- unc ional speci ica ions
Non- unc ional speci ica ions decla e which ope a ional
a ibu es (wha we call
NF-p ope ies)
a e ele an o he
componen being speci ied. NF-p ope ies a e eally
in oduced in
p ope g modules
and hey may be o many
di e en kinds, depending o he domain o hei alues:
boolean (e.g., ull po abili y), nume ical (e.g., deg ee o
eliabili y), eal (e.g., esponse ime), by enume a ion o
alues (e.g., kind o use in e ace -icons, menu, command
language,
...-)
and s ing (e.g., p og amme name)l, and
hey can be a ached o single ope a ions o o whole
modules
(so,
we can alk abou esponse ime o indi idual
ope a ions o abou ull po abili y o a whole module). I
is possible o decla e wha we call
measu emen
uni s,
which ep esen p oblem domain sizes
(e.g.,
numbe
o
books in a lib a y) and ha may be used as cons an
alues, mainly when s a ing e iciency.
Once NF-p ope ies ha e been selec ed, non- unc ional
speci ica ions s a e es ic ions
(NF- equi emen s)
o e he
implemen a ions o he componen .
So,
i is possible o
o mula e NF- equi emen s such as "implemen a ions
mus be ully po able and use in e ace mus be by
means o icons" o "ope a ions mus ha e a esponse ime
no exceeding one second".
2.3.
Implemen a ions
As i has become usual in he componen p og amming
ield, we ha e chosen he objec -o ien ed p og amming
pa adigm o code he implemen a ions. Conce ning
non- unc ional beha iou , i includes: on he one hand,
assignmen o all he NF-p ope ies decla ed in he
non- unc ional speci ica ion; on he o he hand,
equi emen s s a ed o e he implemen a ions o impo ed
componen s o make su e ha he assigned alues eally
hold.
So,
i is possible o s a e hings as: " he esponse
ime o he ope a ion
lis -books
will no exceed one
minu e p o ided ha he so ing algo i hm o he se o
books is no quad a ic o e he size o his se ".
2.4.
An example
We p esen in he nex page ou igu es ha show he
modules o a
NETWORK
componen , which ep esen s
opological ne wo ks (di ec ed g aphs) wi h na numbe s as
nodes, and unlabelled connec ions (edges) be ween hem.
In ig.
1,
we ou line bo h model-o ien ed and algeb aic
speci ica ions (one o hem should be chosen); in he
second case, he keywo d "beha iou al" be o e
op-so
b eaks he de aul ule o in e p e ing he las equa ion
wi h ini ial seman ics. Fig.
2
gi es a non- unc ional
speci ica ion, which a ach he NF-p ope ies decla ed in
some p ope y modules appea ing in ig.
4
o modules and
ope a ions, and adds some addi ional p ope ies; he
measu emen uni s s and o he numbe o nodes and
connec ions in he ne wo k. Las , ig.
3
gi es a beha iou
module o an implemen a ion
IMPL-NETWORK
o
NETWORK;
he NF- equi emen o e
LIST-NAT
mus
be sa is ied by he implemen a ion selec ed o his
componen inside
IMPL-NETWORK.
3.
Ca alogue
o
p ocess
asks
We desc ibe in his sec ion a se o p ocess asks aimed
a suppo ing componen p og amming wi h p o o yping,
and allowing he au oma ic selec ion o implemen a ions
om hei non- unc ional cha ac e is ics. In he gene al
case, p o o yping could in ol e bo h unc ional
speci ica ions and implemen a ions; we ha e explo ed in
p e ious wo ks
[l,
3,
41
he condi ions ha should be
ul illed in o de o ha e success ul p o o yping.
As
we
said in he in oduc ion, he asks iden i ied in his
ca alogue ac as p imi i es
o
ou p ocess language,
in oduced in sec ion
4.
We ha e also
a
special kind o domain o measu ing e iciency,
he domain o he asymp o ic no a ions, ha we do no in oduce he e
o
he sake
o
b e i y.
200
unc ional speci ica ion module
NETWORK
impo s
LIST-NAT
ype
ne wo k
=
V: se -o (na ) x E: se -o (na
x
na )
in a ian
g: ne wo k;
,
w: na
no
( ,
)
in g.E
( ,
w) in g.E
=>
(
in g.V) and
(w
in
g.V)
--
no e lexi e edges
ope a ions
...
add, emo e (ne wo k, na , na )
e u ns
ne wo k
..
beha iou
...
p e and pos condi ions o he ope a ions
{
m
<>
n
and m
in
g.V and
n
in g.V)
{
g'.E
=
union(g.E, single on((m,
n)))}
g'
:=
add(g, m,
n)
...
end
'
module
unc ional speci ica ion module
NETWORK
impo s
LIST-NAT
ype
ne wo k
ope a ions
...
beha iou al
op-so (ne wo k)
e u ns
lis -na
equa ions
...
equa ions o he componen
[belongs(succ(d, m), n)]
=>
be o e( op-so (d), m,
n)
=
ue
end module
Fig.
1:
Two
al e na i e unc ional speci ica ions o a
NETWORK componen .
non- unc ional speci ica ion module
NETWORK
impo s
PORTABILITY, EFFICIENCY,
PROGRAMMER, RELIABILITY
module le el
ully-po able, p og amme -name,
ope a ion le el
ime, space, eliabili y
measu emen uni s
nbnodes, nbconns
equi emen s
ex e nal-p og amme ,
nbconns
<=
pow(nbnodes,
2)
no ully-po able
=>
ex emal-p og amme and no ully-po able
=>
eliabili y(ops(NETW0RK))
<>
high
eliabili y(ops(NETW0RK))
=
low
end module
Fig.
2:
Non- unc ional speci ica ion
o
NETWORK.
beha iou module o
IMPL-NETWORK
ully-po able; no ex e nal-p og amme
p og amme -name
=
"Smi h"
ime(succ)
=
nbnodes;
...
eliabili y(ops(NETW0RK))
=
high,..
equi emen s on
LIST-NAT: ully-po able
end module
Fig.
3:
Beha iou module o a NETWORK
implemen a ion
p ope y module
PORTABILITY
boolean
ully-po able
p ope ies
end module
p ope y module
PROGRAMMER
boolean
ex e nal-p og amme
s ing
p og amme -name
p ope ies
end module
p ope y module
EFFICIENCY
nume ical
ime, space
end module
p ope y module
RELIABILITY
p ope ies
p ope ies
enume
eliabili y
=
(high, medium, low)
end module
Fig.
4:
Some p ope y modules decla ing NF-p ope ies.
Tasks a e module-o ien ed; his is o say, all o hem
a e e e ed o one o mo e modules om all kinds:
unc ional speci ica ion, non- unc ional speci ica ion,
implemen a ion, beha iou and p ope y modules. The
asks p esen ed below may be le empo ally incomple e
while execu ing o he ones,
o
some o hem may be
execu ed simul aneously, p o ided ha ela ionships
be ween asks a e no iola ed (see
3.2).
Also, some o he
asks may be pe o med jus by doing no hing ( o
ins ance, an implemen a ion may be le un es ed).
3.1.
The
asks
Tasks o building modules. We ha e iden i ied:
de ine(M),
o decla e he in e ace o
a
so wa e
componen ;
decla e(P),
o in oduce he name and ype
o one o mo e NF-p ope ies in
a
p ope y module,
and op ionally some NF- equi emen s o e hem;
Fspeci y(M),
o build he unc ional speci ica ion o
a
componen
M;
FNspeci y(M,
Mn ),
o build
a
non-
unc ional speci ica ion
Mn
o
a
componen
M;
implemen (M,
I),
o build an implemen a ion
I
o
a
componen
M;
and
s a e-beha iou (1,
In ,
o s a e he
beha iou
In
o an implemen a ion
1.
These asks
may euse modules om he lib a y wi h he asks
in oduced below.
Lib a y managemen asks. We conside he exis ence
o lib a ies o s o e speci ica ions, implemen a ions
and p ope y modules. Then, we ha e de ined he
ollowing asks:
0
Reusing
a
componen speci ica ion composed by
M
and
Mn
( unc ional and non- unc ional pa s) om
he lib a y
L
in
a
componen speci ica ion
M'.
This
kind o euse may
be
o
h ee
di e en kinds:
201
i
impo (M’,
L,
M,
Mn :
o euse he module
M
wi hou any modi ica ion excep some op ional
enaming.
ii
ins an ia e(M’, L,
M,
Mn ):
o ob ain a
conc e e componen om a gene ic one (e.g., se s
o books om gene ic se s), wi h op ional
enaming.
iii
inhe i (M‘,
L,
M,
MnJ
...)
:
o ob ain
a
new
componen by (possibly mul iple) inhe i ance
om o he ones.
0
Reusing a componen implemen a ion composed by
I
and
I
(code and beha iou module) om he
lib a y
L
in a componen implemen a ion
I‘.
In his
case, only
impo
and
ins an ia e
a e
allowed.
0
Impo ing a p ope y module
P
om he lib a y
L
in
ano he p ope y module
P’: impo (P’,
L,
P).
0
Impo ing a p ope y module
P
om he lib a y
L
inside a non- unc ional speci ica ion
Mn :
a ach(MnJ
L,
P).
0
S o ing a module
X
in o he co esponding lib a y
L: s o e(L,
X).
In he case o speci ica ions and
implemen a ions,
X
include bo h he unc ional and
he non- unc ional pa s.
Ope a ional asks. We include he e p o o yping asks,
implemen a ion selec ion asks and alida ion asks.
0
P o o yping a unc ional speci ica ion
M:
es -spec(M).
Also, he e exis s
es -impl(l),
o
p o o ype an implemen a ion
I.
Bo h asks may
e en ually in ol e mixed execu ion (combining
speci ica ions and code) as explained in
[
1,4].
0
Tes ing i he beha iou module In a ached o an
implemen a ion sa is ies he NF- equi emen s s a ed
in he co esponding non- unc ional speci ica ion
Mn :
NF alida e(Inj
Mn ).
The success o his ask
is necessa y o conside he implemen a ion co ec .
0
Tes ing i an implemen a ion
I
o a componen
M,
wi h NF-beha iou
In ,
sa is ies he NF-
equi emen s s a ed o e
M
inside ano he beha iou
module
In ’:
NF es (ln ,
M,
In ).
The success o
his ask is necessa y o conside
I
as a alid
implemen a ion o
M
in he con ex ep esen ed by
In .
0
Selec ing manually an implemen a ion
I
o a
componen
M,
wi h NF-beha iou In , inside
ano he implemen a ion
I’:
NFmanselec (l’,
I,
In .
0
Selec ing
au oma ically
an
implemen a ion
o
a
componen
M
which sa is ies he NF- equi emen s
s a ed o e
M
inside ano he implemen a ion
I’
wi h
NF-beha iou In :
NFau oselec (In ’,
M).
3.2.
P ecedence
g aphs
I is clea ha he asks iden i ied abo e sa is y some
p ecedence ela ionships ha mus be ollowed in o de o
de elop a co ec design o a so wa e sys em. To
modelise hese ela ionships, we ha e de ined h ee
di e en kind o g aphs, ha we call
p ecedence g aphs,
e e ed o speci ica ions, implemen a ions and p ope y
modules. Each g aph is bound o conc e e modules o he
app op ia e ype;
so,
ela ionships a e module-o ien ed, as
well as asks.
Fig.
5
p esen s he p ecedence g aph o a speci ica ion
wi h unc ional pa
M
and non- unc ional pa
Mn ,
SpecG aph(M,
Mn ).
In e ace de ini ion should p ecede
bo h unc ional and non- unc ional speci ica ions o he
module. To ca y ou p o o yping, unc ional speci ica ion
should be comple e. Once he speci ica ion is comple e, i
may be s o ed in he lib a y in o de
o
be e ie ed o i s
u u e use in o he componen s.
Fig.
7
shows he p ecedence g aph o an
implemen a ion
I
wi h NF-beha iou
In ,
ImplG aph(I,
In ).
I is s a ed ha an implemen a ion (i s code) should
be buil once i s speci ica ion is comple e, and a e wa ds
i s NF-beha iou should be s a ed, and also p o o yping o
he code may be ca ied ou . F om he non- unc ional
speci ica ion and he NF-beha iou , implemen a ion
alida ion is possible and i mus p ecede s o age in he
lib a y.
Las , ig.
6
shows he g aph o a p ope y module
P,
P opG aph(P).
As
he ones be o e, i is s a ed ha a
module should be comple ed be o e s o ing i in he
lib a y, and hen i may be impo ed by o he p ope y
modules o i may be a ached o a pa icula
non- unc ional speci ica ion.
Fspeci y(M) NFspeci y(M, Mn )
es -spec(M) s o e(SpecLib,
M,
Mn )
impo /ins an ia e/inhe i (M’,
SpecLib, M, Mn )
Fig.
5:
P ecedence g aph a he specijica ion le el.
decla e(P)
s o e(P opLib, P)
impo (P, P opLib, P)
Fig.
6:
P ecedence g aph a he p ope y le el.
a ach(Mn , P opLib,
P)
202
NFspeci y(M,
Mn )
Fspeci y(M)
implemen (M,
I)
s a e-beha iou (I',
In )
NF es (In ,
M,
In )
es jmpl(1) s a e-beha iou (1, In )
NFau oselec (In ,
M)
s o e(ImplLib,
I,
In )
NF alida e(In ,
J
Mn )
NFmanselec (I',
I,
Inn
euse/ins an ia e(I', ImplLib,
I,
In )
Fig.
7:
P ecedence g aph a he implemen a ion le el.
4.
So wa e p ocess models
Once we ha e de ined he ca alogue o exis ing asks
and he ela ionships hey should ollow
in
sys em
de elopmen , we ocus in he p oblem o how o de ine
conc c e so wa e p ocess modcls.
As
said in he
in oduc ion, we ocus in ou pa icula phases o so wa e
p ocess: speci ica ion, design, implemen a ion and es ing;
howe e , we will con inue using he e m "so wa e
p ocess"
as
a
sho hand o hese phases.
Gi en he modelisa ion o p ecedence ela ionships
using g aphs, we can conside a de elopmen s a egy
as
a
se o new edges binding nodes o hese g aphs.
Some imes, edges will ela e asks (nodes) in he same
g aph, o say hings like " he unc ional speci ica ion o
a
componen mus be de eloped be o e he non- unc ional
one"; howe e , in he gene al case, edges will in ol e
asks appea ing in g aphs bound o di e en modules, as in
"i is necessa y o speci y all he componen s impo ed by
a
componen
M
be o e any implemen a ion o
M
is buil ".
Also, we de ine
a
kind o g ouping mechanism o allow
he s a emen
o
ac s
as
" unc ional and non- unc ional
speci ica ion o
a
componen mus ake place
as
a
whole".
As
a
esul , we iden i y wo di e en elemen s o
o mula e de elopmen s a egies: ules and g oupings,
which
a e
in oduced in
4.1
and
4.2.
4.1.
Rules
o
p ecedence
A so wa e p ocess model
is
mainly cha ac e ised by
some pa icula p ecedence ela ionships be ween asks.
We de ine hese ela ionships
as
a pai (called
ule
he ea e )
le
->
igh ,
whe e
le
and
igh
a e se s o
asks.
The
meaning o he ule is: i he asks appea ing in
le
ha e been comple ed, hen all he asks appea ing in
igh
can s a o be execu ed; in o he wo ds, he ule
is
adding an edge om e e y ask (node) appea ing in
le
o
e e y ask appea ing in
igh .
Once again, le 's ema k ha
asks a e de ined a module le el;
as
a
esul , ules will be
pa ame e ised by he modules appea ing in asks.
We de ine he ollowing elemen s o w i e ules:
Iden i ie s o ep esen module names.
A quan i ie o he o m:
meaning ha he ule holds jus o he speci ied
se o modules.
Some buil -in unc ions o ob ain se s o modules
ela ed somehow wi h
a
gi en one.
Fig.
8
shows an example. So wa e p ocess models a e
encapsula ed in
s a egy modules.
I is possible o
combine exis ing s a egy modules o o m new ones,
adding op ionally new ules and g oupings. This p ope y
suppo s inc emen al de elopmen o s a egies
as
combina ion o simple ones, and imp o es
unde s andabili y and eusabili y o he modules. The i s
s a egy module o ces unc ional speci ica ion o
componen s o be ca ied ou be o e non- unc ional one.
This is a
ule
ha add edges in single g aphs, he ones o
componen speci ica ions,
as
we show in he i s g aph o
ig.
8.
The second s a egy de e mines
a
kind o bo om-up
speci ica ion s a egy: be o e speci ying
a
module
M,
i
is
necessa y o speci y all he modules used by
M;
so,
many
g aphs a e in ol ed, and we show in ig.
8
he
speci ica ion g aphs o
a
sys em wi h h ee speci ica ions
(including unc ional and non- unc ional pa s)
(A,
Anj),
(B,
Bnj)
and
(C,
Cnj)
such ha
(A,
Anj)
uses he o he
ones. Las , he hi d s a egy module combines he
p e ious ones, yielding o
a
kind
o
bo om-up
speci ica ion de elopmen s a egy ha gi es p ecedence o
he unc ional pa . We omi a iable decla a ions.
Tasks, pa ame e ised by modules.
o
all
x
in
se o modules: ule(x)
203

s a egy
FUNCTIONAL-BEFORE-NON-FUNCTIONAL
end module
Fspeci y(M)
->
NFspeci y(M)
s a egy
BOTTOM-UP-SPECIFICATION
o
all
Z in
used-in()():
Fspeci y(Z)
->
Fspeci y(X), NFspeci y(X, Xn )
NFspeci y(Z, Zn )
->
NFspeci y(X, Xn )
end module
s a egy
BOTTOM-UP-WITH-FUNCTIONAL-BEFORE
combines
FUNCTION
AL-BEFORE-NON-FUNCTIONAL,
BOTTOM-U€-SPECIFICATION
end module
de ine(M)
Fspeci y(M)
+
NFspeci y(M, Mn )
es -spec(M) s o e(SpecLib,
M,
Mn )
J.
impo /ins an ia e/inhe i (M',
SpecLib, M, Mn )
SpecG aph(B, Bn ) SpecG aph(C, Cn )
de ine(C)
Fspeci y (C) NFspeci y(C, Cn )
Fspeci y(
A)
NFspeci y(A, An )
I
I
...
...
SpecG aph(A, An )
Fig.
8:
Th ee s a egy modules and he speci ica ion g aph esul ing om he i s
wo
o
hem.
4.2.
G ouping
o
asks
We in oduce he e some no a ion o co e he need o
g ouping some ela ed asks, all o hem usually e e ed o
he same module. This g ouping is exp essed
by
enclosing
he se o asks be ween pa en hesis,
( askl,
...,
askn).
The meaning o his g ouping
is:
once a ask om
askl,
...,
askn
is s a ed, de elopmen mus comple e all o
hem be o e s a ing any o he ask. Tasks in a g ouping
may e e o a subse o modules, using he same
quan i ie as ules.
No e ha g ouping does no s a e no hing abou o de
o execu ion o hese asks ( his is done using ules); also,
no e ha g ouping does no oblige nei he
o
comple e
a
ask be o e s a ing o he s o he g oup no he o he way
ound ( o ins ance, he
n
asks may be simul aneously in
execu ion i ules allow his si ua ion). Las , we ema k
ha g oupings can be o mula ed in e ms o asks: a
g ouping
( askl,
...,
askn)
adds an edge om e e y
p edecesso o e e y ask in
askl,
...,
askn
o e e y
successo
o
e e y ask in
askl,
...,
askn; so,
he
n
asks
mus in allibly be ca ied ou as a whole.
Fig.
9
shows wo examples o g ouping and i s
combina ion wi h ules. The i s s a egy module o ces
unc ional and non- unc ional speci ica ion o a componen
o be pe o med as
a
whole.
As
he speci ica ion g aph o
he componen does no include any p ecedence
ela ionship be ween hese wo asks, any o de o
execu ion and s a e o comple ion is possible. Bu i we
conside
a
de elopmen s a egy combining his g ouping
204
and he
FUNCTIONALBEFORE-NON-FUNCTIONAL
s a egy (see ig.
S),
he esul is a new s a egy ha
equi es, when speci ying e e y componen in he sys em,
o comple e he unc ional pa and immedia ely he non-
unc ional one; no e he di e ence wi h he s a egy
FUNCTIONAL-BEFORE-NON-FUNCTIONAL
alone,
ha allows o ca y ou o he asks be ween unc ional and
non- unc ional speci ica ions. Las , he s a egy
SPECIFICATION-OF-USED-MOD ULES
shows he use
o quan i ie s in g ouping; he module s a es ha all
unc ional speci ica ions o impo ed componen s mus
ake place indi isibly; his module could combine wi h
BOTTOM-UP-SPECIFICATION
o o m a new s a egy.
s a egy
WHOLE-SPECIFICATION
end module
(Fspeci y(M), NFspeci y(M, Mn ))
s a egy
WHOLE-SPECIFICATION-FUNCTIONAL-
1
ST
combines
FUNCTIONAI-BEFORE-NONJU"ONAL,
WHOLE-SPECIFICATION
end module
s a egy
SPECIFICATION-OF-USED_MODULES
end module
( o
all
Z
in
used-in(M): Fspeci y(Z))
Fig.
9:
Two new s a egy modules wi h g ouping.
5.
Co ec ness o so wa e de elopmen s
In his sec ion, we a e going o de ine o mally he
no ion o co ec ness o a sys em so wa e de elopmen
wi h espec o a so wa e p ocess model2. Fi s , we
p opose a model o sys em so wa e de elopmen s as a
sequence o asks.
A
so wa e sys em de elopmen is a sequence o asks
such ha he e
a e
no epea ed asks:
i
#
j
whe e " i
j" means ha i and j canno be he same ask
applied o he same module(s).
0
Nex , we o malise he no ion o so wa e p ocess
model as a pai o se s, a se o ules and a se o
g oupings. Then, we de ine he g aph bound o a so wa e
sys em de elopmen as a g aph including as many
subg aphs as modules appea in
s
(see
3.2)
and
inco po a ing di ec ed edges be ween nodes gi en bo h he
se o ules and he se o g oupings o he p ocess model,
as explained in sec ion
4.
Las , we o mula e he no ion o
De ini ion
1.
So wa e sys em de elopmen .
SSde
=
( ask)*
/
V's~SSde :
s
=
i
...
k: i #j
We
do no ocus
he e
on unc ional and non- unc ional
co ec ness
o
he sys em i sel , which may be s udied h ough classical
p oo obliga ions. Also, we do no add ess he e
o
comple eness
o
so wa e sys ems de elopmen s, de ined
as
he exis ence
o
implemen a ions enough o ob ain
a
comple ely implemen ed sys em
sa is ying all he equi emen s s a ed in beha iou modules.
co ec ness o a so wa e sys em de elopmen wi h espec
o a p ocess model in e ms o a opological
so
o e he
esul ing g aph.
A
so wa e p ocess model
g
is a pai ,
g
=
(S ,
Sg),
such
ha
S
is a se o ules and
Sg
a
se o g oupings:
De ini ion
2.
So wa e p ocess model.
S
E
e( ask)*
x
( ask)")
A
Sg
E
ee ask))
0
De ini ion
3.
G aph induced by se s o modules,
ules and g oupings.
Le
S,
S
and
Sg
be se s o modules (in he case o
speci ica ions and implemen a ions, pai s o modules
including unc ional and non- unc ional pa s), ules and
g oupings, espec i ely. We de ine he g aph induced by
S,
S
and
Sg,
G aph(S,
S ,
Sg),
as he minimum g aph
sa is ying:
VM, Mn (M, Mn )ES
A
M and Mn o m a speci ica ion:
SpecG aph(M, Mn )
E
G aph(& S , Sg)
ImplG aph(1, In )
c
G aph(& S , Sg)
P opG aph(P)
c
G aph(S, S , Sg)
VI,
In (I, 1n )E
S
A
I and In o m an implemen a ion:
VP: PE
S
A
P is a p ope y module:
*V : ES A =(l-> ):
Vx, y: x~l
A
yE :
Vassignmen
a
o
he modules
o
x and y
wi h alues om
S,
x[al and y[al:
he edge
(x[S]
->
y[S]) is in G aph(& S , Sg)
Vg: g€ sg
A
g
=
( l,
...,
k):
Vi,j:
1
I
i,j
I
k
A
i
#j:
Vassignmen
a
o he modules o i and j
(VX,~: he edges (X
->
i[a]) and ( j[a]
->
Y)
he edge (x
->
y) is in G aph(S, S , Sg)
whe e
SpecG uph(M,
Mn ),
ImplG aph(I, In )
and
P opG uph(P)
a e de ined as in
3.2.
We assume ha
quan i ica ions implici ly expand o se s o ules and
g oupings.
0
De ini ion
4.
Co ec ness o a so wa e sys em
de elopmen wi h espec o
a
so wa e p ocess model.
Le
s
=
i
..&E
SSde be a so wa e sys em de elopmen
and le
g
=
(S ,
Sg)
be
a
so wa e p ocess model. We say
ha
s
is
co ec
wi h espec o
g
i s ollows
a
alid
opological so a e sal o he g aph induced by
g
and he
modules o
s:
SE
TopSo (G aph(Modules(s),
S , Sg)),
whe e Modules(s) gi es he se o modules in oduced in
s
and Topso @ gi es he se o alid opological so
a e sals o e he g aph
0
wi h alues om
S,
i[a] and j[a]:
a e in G aph@, S , Sg)):
205
6.
Conclusions
p esen ed he e: model-o ien ed o algeb aic
speci ica ions and objec -o ien ed p og amming.
We ha e p esen ed a p oposal o o mula e so wa e
p ocess models in he componen p og amming
amewo k. This p oposal elies on he exis ence
o
a
ca alogue o asks o build he componen s, o p o o ype
hem, o selec he app op ia e implemen a ions o hem
and o s o e hem and o e ie e hem ol om lib a ies;
his asks p esen p ecedence ela ionships be ween hem.
So wa e p ocess models a e encapsula ed in o s a egy
modules, which consis s
o
a se o ules (new p ecedences
be ween asks) and a se o g oupings ( asks ha mus be
conside ed as a whole). Finally, i has been o mally
in oduced he no ion o co ec ness o a so wa e
de elopmen wi h espec o a so wa e p ocess model,
based in a g aph ep esen a ion o p ocess models.
The e a e many aspec s
o
ou wo k ha ha e no been
included in he pape . Fi s , he no ion o componen
ede elopmen , which equi es ede ining sligh ly he
de ini ion o so wa e sys em de elopmen . Also, we do
no include he comple e de ini ion o co ec ness, aking
in o accoun unc ional and non- unc ional co ec ness.
Las , we ha e no shown he decomposi ion o asks in o
sub asks. Ano he in e es ing poin is he use o he
de elopmen sequence as a sc ip o analyse he so wa e
p ocess and, e en ually, o eplay i in he u u e
[5,
141.
We hink ha he mos in e es ing poin s o ou
app oach a e he ollowing ones:
The p ocess language consis s o e y ew
elemen s o make i ease o lea n and use: a small
ca alogue o asks wi h well-de ined ela ionships,
wo mechanisms o ela e asks ( ules and
g oupings) and a ew addi ional cons uc ions
(quan i ica ion and p ede ined unc ions).
So wa e p ocess models may be de ined
inc emen ally, om he combina ion o small
s a egy modules, each one o hem add essing o
pa icula poin s o he model. We may say ha
ou p ocess model language alls in o componen
p og amming a he p ocess le el and,
so,
he
bene i s in his ield also apply o ou p oposal.
A o mal no ion o co ec ness has been de ined.
We belie e ha co ec ness in he p ocess le el is
as impo an as co ec ness in he p oduc le el.
Ou wo k aims a ea ing bo h le els uni o mly.
Non- unc ional equi emen s o so wa e a e aken
in o accoun du ing so wa e de elopmen . This
aspec has no been s udied in de ail he e, bu is a
basic one in ou p ojec
[4,
61:
we belie e ha
non- unc ionali y is as impo an as unc ionali y
and his equi es explici ea men in he p ocess
model.
Al hough he p oposal has been p esen ed o an
ad
hoc
no a ion, i does no eally depend on i ;
so,
he p oposal may be adap ed o e e y
( unc ional) speci ica ion and p og amming
languages wi h simila cha ac e is ics o he ones
Re e ences
[l]
X
Bu gu s,
X.
F anch. "E alua ion o Exp essions in a
Mul ipa adigm F amewo k". In
P oceedings
o
7 h PLILP,
U ech (The Ne he lands), LNCS 982, Sp inge Ve lag, 1995.
[2]
E.
Dubois, A. an Lamswee de. "Making Speci ica ion
P ocesses Explici ". In
4 h In e na ional Wo kshop
on
So wa e Speci ica ion and Design,
Mon e ey (U.S.A.), 1987.
[3]
X.
F anch,
X.
Bu guCs.
"A
Case S udy on P o o yping
wi h
Speci ica ions".
P ocs. Wo kshop on De elopmen and
T ans o ma ion
o
P og ams,
Nancy (F ance), 1993.
[4]
X.
F anch,
X.
Bu guCs. "Inc emen al Componen
P og amming wi h Func ional and Non-Func ional
In o ma ion". In
P oceedings
o
XVI In l. Con e ence
o
Chilean Compu ing Science Socie y,
Valdi ia (Chile), 1996.
[5]
X.
F anch, P. Bo ella. "P o o ipado de P og amas
usando Especi icaciones Funcionales
y
No Funcionales"
(w i en
in
Spanish). In
Ac as de las P ime as Jo nadas de
T ubajo en Ingenie ia del So wa e,
Se illa (Espaiia), 1996.
[6]
X.
F anch, P. Bo ella. "Suppo ing So wa e
Main enance wi h Non-Func ional In o ma ion". In
P oceedings 1s EUROMICRO Con e ence on So wa e
Main enance and Reenginee ing,
Be lin (Ge many), 1997.
[7] A. Finkels ein, J. K ame , B. Nuseibeh.
So wa e
P ocess Modelling and Technology.
J.
Wiley
&
sons, 1994.
[8] J.V. Gu ag, J.J. Ho ning.
La ch: Languages and Tools
o
Fo mal Speci ica ion.
Tex s and Monog aphs
in
Compu e
Science, Sp inge -Ve lag.
[9] J.A. Goguen
e al.
"In oducing OBJ3". D a Repo ,
SRI In e na ional, 1993.
[IO]
M. Jazaye i. "Componen P og amming
-
a F esh
Look a So wa e Componen s". In
P oceedings
o
5 h ESEC,
Ba celona (Ca alonia, Spain), 1995.
[
111
C.B. Jones.
Sys ema ic So wa e De elopmen using
VDM.
P en ice-Hall, 1990.
[
121 B. K ieg-B uckne (ed.).
P og am de elopmen by
Speci ica ion and T ans o ma ion.
LNCS 680, Sp inge
Ve lag, 1993.
[13]
L.
Os e weil. "So wa e P ocess a e So wa e
Too".
In
P oceedings o 9 h ICSE,
Mon e ey (U.S.A.), 1987.
[
141 M. Sin zo . "Exp essing P og am De elopmen s
in
a
Design Calculus". In
P ocs. o he ln l. Summe School
on
Logic
o
P og amming,
NATO AS1 Se ies, Vol F36, Sp inge
Ve lag, 1987.
[
151
M. Si a aman (coo dina o ). "Special Fea u e:
Componen -Based So wa e Using RESOLVE". ACM So wa e
Enginee ing No es, 19(4), Oc . 1994.
[16] J.M. Spi ey.
The
Z
No a ion.
P en ice-Hall, 1993.
[17] M. Saeki,
K.
Wenyin. "Speci ying So wa e
Speci ica ion and Design Me hods". In
P oceedings
o
6 h
CAiSE,
U ech (The Ne he lands), LNCS 81
1,
1994.
[
181 D. Wile. "P og am De elopmen s: Fo mal
Explana ion o Implemen a ions". In
New Pa adigms o
So % a e De elopmen s,
IEEE Compu e Socie y P ess, 1986.
206