Software process modelling as relationships between tasks

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