The ISPW7-Example Solution Dewayne E. Perry Software Principles Research Department Software & Systems Research Center AT&T Bell Laboratories 600 Mountain Avenue Murray Hill NJ 07974 Interact is a (generally) non-procedural, goal-directed process modeling language that is coupled with a pro-active process support environment Intermediate. Together they provide an environment for the description of process models, their administration, customization, evolution and enactment. There are three parts present in an Interact process model: the organization and product models, the policies that express various facts and relationships about the organization, product and process state. In particular, policies are used to define modes of interaction and communication among the implementors in a software process. The activities are defined in terms of their assumptions (expressed in terms of policies) and results expressed in terms of the policies satisfied and policies obligated to be satisfied (one or more of which results may be instantiated concurrently). The Intermediate support environment provides support for model administration (populating various objects in the model, determining which definitions for various policies prevail, instantiating activities, etc.), process enactment, maintenance of process state and history, and providing process guidance to the process user. Summary of the Interact/Intermediate solution to the ISPW7 example: 1. I addressed all of the extensions. See the model and the appendix. 2. I spent 3 full days of work spread over 5 working days (9/25 - 1/2, 9/26 - 1/2, 9/27 - 1/2, 9/30 - 3/4, 10/1 - 3/4) 3. The ISPW6 example was extensively reused: about 1/4 day was spent updating the ISPW6 example to the current syntax of Intermediate and the currently preferred design and style; about 1 day was spent modifying the organization and product models to support the ISPW6/ISPW7 extensions; about 1 day was spent modifying the policies to support the ISPW6/ISPW7 extensions; and about 3/4 day was spent reworking the activity descriptions, more than half of which was spent on just the managing part of the process model ( the scheduling/assigning, monitoring, and rescheduling/ reassigning of tasks. 4. In general the approach that I have formulated in Interact/Intermediate lent itself to a succinct description of the process. I was surprised, however, at how much of what i would consider to be Intermediate details (ie, the dynamic aspects of the process support) needed to be included in what I would consider the Interact portion of the model (ie, the static part). This was due primarily to the detailed description of the instantiation, assignment, and scheduling of activities needed to describe the management part of the process model. 5. Most of the current details of the modeling language and environment had been solidified through various other examples and discussions throughout the year. Thinking about this example did, however, crystalize my thinking about the basic processing entities, person and tool. Model Modify-System -- there are two basic processor types: -- person -- tool -- Organization Model type role primitive role ccb-manager role ccb-member role project-manager role software-engineer role design-engineer role quality-engineer type task primitive task modify-design task review-design-mods task modify-code task review-code-mods task modify-mod-test-plans task modify-sys-test-plans task review-mod-test-plans task review-sys-test-plans task test-module task test-system type group set of person type roled-group set of (person, role) type des-rev-team roled-group type task-role (task, role) type task-schedule (task, name, person, date) type task-sched-set set of task-schedule type task-assmnt (activity-id, task, name) type task-assmnt-set set of task-assmnt type module-owner (module-name, person) type mod-owner-set set of module-owner[module-name] type module-drt (name, des-rev-team) type module-drt-set set of module-drt[name] type event primitive event activity-late event person-leave event person-arrive event add-module type event-set set of event type effort days type task-effort (task, effort) type task-effort-set set of task-effort[task] type time-available (person, effort) type time-avlbl-set set of time-available[person] type project-span (date, date) object cc-board roled-group object project roled-group object module-owners mod-owner-set object mod-chg-list module-name-set object review-teams module-drt-set object per-constraints time-avlble-set object effort-per-task task-effort-set object task-roles task-role-set object project-dates project-span object task-schedules task-sched-set object tasks-assigned task-assmnt-set -- Product Model -- type version-id primitive type name text type module-name name type system-name name type modnam-vid (module-name, version-id) type requirement text type req-document seq of requirement type design-decision text type design-doc set of design-decision type system-arch (system-name, design-doc) type module-design (module-name, design-doc) type system-design (system-arch, set of module-design[module-name]) type source-line text type module-source (module-name, seq of source-line) type system-source set of module-source[module-name] type module-dep (module-name, set of module-name) type module-dep-set set of module-dep[module-name] type object-code primitive type module-object (module-name, object-code) type system set of object-code[module-name] type test-input primitive type test-output primitive type test seq of test-input type test-result (*test, seq of test-output) type test-suite set of test type module-tests (module-name, *test-suite) type mod-tests-set set of module-tests[module-name] type system-tests (system-name, *test-suite) type test-driver seq of source-line type test-stub (module-name, seq of source-line) type test-harness (test-driver, set of test-stub[module-name]) type module-harness (module-name, test-harness) type mod-harnesses set of module-harness[module-name] type system-harness (system-name, test-harness) type defect-descr text type defect-list set of defect-descr type mod-defect (name, defect-list) type mod-defect-set set of mod-defect[name] type archived-design (version-id, system-design, date-time, version-id) type archived-source (version-id, system-source, date-time, version-id) type archived-tests (version-id, test-suite, date-time, version-id) type archived-harness(version-id, (name, test-harness), date-time, version-ic) object new-reqs req-document object mod-sys-design system-design object sysdesign-base version-id object mod-sys-source system-source object syssource-base version-id object module-deps module-dep-set object mod-modhars mod-harnesses object modhar-bases set of modname-vid[module-name] object mod-syshar system-harness object syshar-base version-id object mod-mtests mod-tests-set object mtests-bases set of modname-vid[module-name] object mod-stests system-tests object stests-base version-id object module-defects mod-defect-set object test-defects mod-defect-set object design-cm set of archived-design object source-cm set of archived-source object tests-cm set of archived-tests object harness-cm set of archived-harness -- Policy Definitions: policy approve-installation ( person p, object o ) :: primitive policy approve-suspension (person p, object o) :: primitive policy approve-resumption (person p, object o) :: primitive policy approve-cancellation ( person p, object o ) :: primitive policy ccb-authorization ( req-document rc ) :: 1: each (person p, role r) in cc-board, approve-installation(p, rc) 2: (p, ccb-manager) in cc-board and approve-installation(p, rc) policy ccb-suspension ( req-document rc ) :: 1: each (person p, role r) in cc-board, approve-suspension(p, rc) 2: (p, ccb-manager) in cc-board and approve-suspension(p, rc) policy ccb-resumption ( req-document rc ) :: 1: each (person p, role r) in cc-board, approve-resumption(p, rc) 2: (p, ccb-manager) in cc-board and approve-resumption(p, rc) policy ccb-cancellation ( req-document rc ) :: 1. each (person p, role r) in cc-board, approve-cancellation(p, rc) 2. (p, ccb-manager) in cc-board and approve-cancellation(p, rc) policy module-design-modified( module-design md ) :: primitive policy module-source-modified( module-source ms ) :: primitive policy module-interface-modified( module-source ms ) :: primitive policy module-tests-modified( module-tests mt ) :: primitive policy module-harness-modified( module-harness mh ) :: primitive policy system-tests-modified( system-tests st ) :: primitive policy system-harness-modified( system-harness sh ) :: primitive policy dependencies-determined( module-dep md ) :: primitive policy verbal-approval ( person p, object o) :: primitive policy written-approval ( person p, object o ) :: primitive policy consensus ( group g, object ob ) :: 1. each p in g, verbal-approval(p, ob) 2. each p in g, written-approval(p, ob) policy module-design-approved ( roled-group drt, module-design nd ) :: 1. consensus( {person p | (p,*) in drt}, md ) policy module-code-approved ( roled-group rg, module-source ms ) :: 1. consensus( { p | (p,project-manager) in rg or (p,design-engineer) in rg }, ms ) policy module-interface-approved ( group g, module-source ms ) :: 1. consensus( g, interface( ms ) ) policy module-testsuite-approved ( roled-group rg, module-tests mt ) :: 1. consensus( { p | (p,project-manager) in rg or (p,quality-engineer) in rg }, mt ) policy module-testharness-approved ( roled-group rg, module-harness mh ) :: 1. consensus( { p | (p,project-manager) in rg or (p,quality-engineer) in rg }, mh ) policy system-testsuite-approved ( roled-group rg, system-tests st ) :: 1. consensus( { p | (p,project-manager) in rg or (p,quality-engineer) in rg }, st ) policy system-harness-approved ( roled-group rg, system-harness sh ) :: 1. consensus( { p | (p,project-manager) in rg or (p,quality-engineer) in rg }, sh ) policy module-design-review-completed (req-document rc, module-design md ) :: primitive policy module-code-review-completed (module-design md, module-source ms ) :: primitive policy module-interface-review-completed (module-design md, module-source ms ) :: primitive policy module-test-plan-review-completed (req-document rc, module-design md, module-tests mt, module-harness mh) :: primitive policy system-test-plan-review-completed (req-document rc, system-design sd, system-tests st, system-harness sh) :: primitive policy asserted-satisfaction( object o1, o2) :: primitive policy demonstrated-satisfaction( object o1, o2) :: primitive policy verified-satisfaction( object o1, o2) :: primitive policy satisfies ( object o1, o2 ) :: 1. asserted-satisfaction(o1, o2) 2. demonstrated-satisfaction(o1, o2) 3. verified-satisfaction(o1, o2) policy requirements-satisfied ( req-document rc, system-design ((sn,sd),mdset) ) :: 1. each requirement r in rc, some (mn, md) in mdset, d in md and satisfies(d, r) or some d in sd, satsifies(d, r) policy design-satisfied ( module-design (mn,md), module-source (mn,sl) ) :: 1. each design-decision d in md, some seq of source-line s in sl, satisfies(s, d) policy asserted-coverage( module-tests mt, module-source ms) :: primitive policy coverage-results( module-tests mt, module-source ms, real mc) :: primitive policy covers( module-tests mt, module-source ms ) :: 1. asserted-coverage(mt, ms) 2. coverage-results(mt, ms, 90%) policy test-satisfied( module-name mn, test t) :: primitive policy module-tests-satisified (module-name mn, test-suite ts) :: 1. each t in ts, test-satisfied(mn, t) policy module-testing-completed ( mod-tests-set mts ) :: 1. each (mn, ts) in mts, module-tests-satisfied(mn, ts) policy system-tests-satisfied ( system-tests (sn, ts ) ) :: 1. each t in ts, test-satisfied(sn, t) policy system-testing-completed ( module-tests-set mts, system-tests st ) :: 1. module-testing-completed(mts) and system-tests-satisfied(st) policy remedies( object o1, o2) :: 1. asserted-remediation(o1, o2) 2. demonstrated-remediation(o1, o2) 3. verified-remediation(o1, o2) policy design-defects-remedied ( defect-list dl, design-doc dd ) :: 1. each defect-descr def in dl, some design-choice dc in dd, remedies(dc, def) policy code-defects-remedied ( defect-list dl, module-source ms ) :: 1. each defect-descrd in dl, some seq of source-line s in ms, remedies(s, d) policy interface-defects-remedied ( defect-list dl, module-source ms ) :: 1. each defect-descrd in dl, some seq of source-line s in ms, remedies(s, d) policy test-defects-remedied(defect-list dl,test-suite ts,test-harness (td,tsset) :: 1. each defect-descr in dl, some test t in ts, remedies(t, d) or some seq of source-line s in td, remedies(s, d) or some (mn,sl) in tsset, some seq of source-line in sl, remedies(s, d) policy module-modification-completed (module-design md, module-source ms, mod-harness mh, mod-tests-set (mn, ts) ) :: 1. module-testing-completed(m, ts) 2. module-design-approved(project, md) and module-code-approved(project, mts) and module-harness-approved(project, mh) and module-testsuite-approved(project, (mn,ts)) and module-tests-completed(mn, ts) policy system-modification-completed (reqs-document rc, system-design (sa, mds), system-source ss, system-harness sh, system-tests (sn, ts), mod-harnesses mh, mod-tests-set mts ) :: 1. system-tests-satisfied(sn, ts) and each module-tests (mn, mt) in mts, module-modification-completed(mds[mn],ss[mn],nh[mn],(mn,ts)) 2. requirements-satisfied ( rc, (sa, mds )) and system-harness-approved ( project, sh ) and system-testsuite-approved ( project, ts ) and system-tests-satisfied (sn, ts) and each module-tests (mn, mt) in mts, module-modification-completed(mds[mn],ss[mn],nh[mn],(mn,mt)) policy tasks-scheduled( task-role-set tr, task-sched-set ts ) :: 1. each (t, r) in tr some person p, (t, m, p, d) in ts and (p, r) in project 2. each (t, r) in tr some person p, (t, m, p, d) in ts and project == { (p,r) | (t,m,p,d) in ts and (t,r) in tr } policy schedule-is-date-consistent ( task-sched-set ts, project-span (ps, pe)) 1. each date d in { d | (t, m, p, d) in ts }, ps <= d <= pe policy schedule-is-effort-constrained (roled-group pr, task-sched-set ts, task-effort-set ept, time-avlbl-set tas, project-span (ps, pe)) :: each person p in { p | (p,r) in pr }, sum == add( {eft[t] | (t, m, p, d) in ts} ) and sum <= tas[p] and sum' <= (pe - ps) + 1 policy schedule-is-path-consistent (roled-group pr, task-sched-set ts, task-effort-set ept, time-avlbl-set tas, project-span (ps,pe)) :: 1. each person p in { p | (p,r) in pr }, each d in ordered-seq( { d | (t,m,p,d) in ts} ), sum == add({eft[t] | (t,m,p,de) in ts and de <= d}) and sum <= (d - ps) + 1 policy schedule-satisfactory (roled-group pr, task-sched-set ts, taks-effort-set ept, time-avlbl-set tas, project-span ps) :: 1. schedule-is-date-consistent( ts, ps ) and schedule-is effort-constrained( pr, ts, ept, tas ) and schedule-is-path-consistent( pr, ts, ept, tas, ps ) policy notified (person p, message m) :: primtive policy notified-of-assignment ( person p, task t, date d, module-name ) :: 1. notified (p, "Assignment: task %t for module %mn, due %d.") policy notified-of-retraction ( person p, task t, date d, module-name ) :: 1. notified (p, "Cancel assignment: task %t for module %mn, due %d.") policy personnel-notified-of-assignments( set of task-sched-set tss ) :: 1. each (t, mn, p, d) in tss, notified-of-assignment(p,t,d, mn) policy personnel-notified-of-reassignments ( task-sched-set oldts, task-sched-set newts ) :: 1. each (t, mn, p, d) in oldts notified-of-retraction(p,t,d, mn) and each (t, mn, p, d) in newts, notified-of-assignment(p,t,d, mn) policy dependencies-notified-interface-change ( module-dep (mn, ml ) ) :: 1. each m in ml, notified (module-owners[m], "Interface for module %mn has changed" ) policy pm-notified ( message m ) :: 1. some (p,r) in project, r == project-manager and notified( p, m ) policy pm-notified-of-design-review ( module-name mn, date-time dt ) :: 1. pm-notified( "design review completed for module %mn at %dt" ) policy pm-notified-of-code-review ( module-name mn, date-time dt ) :: 1. pm-notified( "code review completed for module %mn at %dt" ) policy pm-notified-of-interface-review ( module-name mn, date-time dt ) :: 1. pm-notified( "interface review completed for module %mn at %dt" ) policy pm-notified-of-module-test-plan-review ( module-name mn, date-time dt ) :: 1. pm-notified( "test plan review completed for module %mn at %dt" ) policy pm-notified-of-module-tested ( module-name mn, date-time dt ) :: 1. pm-notified( "testing completed for module %mn at %dt" ) policy pm-notified-of-system-test-plan-review ( system-name sn, date-time dt ) :: 1. pm-notified( "test plan review completed for system %sn at %dt" ) policy pm-notified-of-system-tested ( system-name sn, date-time dt ) :: 1. pm-notified( "testing completed for system %sn at %dt" ) policy compiled-errorfree ( module-source ms ) :: primitive policy compiled-with-errors ( module-source ms, defect-list errors ) :: primitive policy design-archived ( system-design sd, date-time dt, version-id base ) :: 1. design-cm' == design-cm + ( new-design-version(), sd, d, base ) policy source-archived ( system-source ss, date-time dt, version-id base) :: 1. source-cm' == source-cm + ( new-source-version(), ss, d, base ) policy tests-archived ( test-suite ts, date-time dt, version-id base) :: 1. tests-cm' == tests-cm + ( new-tests-version(), ts, d, base ) policy harness-archived ( test-harness th, date-time dt, version-id base) :: 1. harness-cm' == harness-cm + ( new-harness-version(), th, d, base ) -- Activity Definitions: activity Manage-Project() preconditions: (SELF, project-manager) in project { sequence: Schedule-Tasks ( task-roles, task-schedules, task-assigned, effort-per-task, per-constraints, project-dates ) Assign-Tasks ( task-roles, task-schedules, task-assigned, effort-per-task, per-constraints, project-dates ) iterate Monitor-Tasks ( task-roles, task-schedules, task-assigned, effort-per-task, per-constraints, project-dates ) until system-modification-completed(new-reqs,mod-sys-design,mod-sys-source, mod-syshar,mod-stests,mod-modhars,mod-mtests) or ccb-cancellation( new-reqs ) } 1. postconditions: system-modification-completed(new-reqs,mod-sys-design,mod-sys-source, mod-syshar,mod-stests,mod-modhars,mod-mtests) obligations: 2. postconditions: ccb-cancellation( new-reqs ) obligations: activity Schedule-Tasks ( task-role-set trs, task-sched-set ts, task-assmnt-set ta, task-effort-set ept, time-avlble-set tas, project-span ps ) preconditions: ccb-authorization(new-reqs) { primitive } results: 1. postconditions: tasks-scheduled( trs, ts) schedule-satisfactory( project, ts, ept, tas, ps ) obligations: personnel-notified-of-assignments(ts) activity Assign-Tasks ( task-role-set trs, task-sched-set ts, task-assmnt-set ta, task-effort-set ept, time-avlble-set tas, project-span ps ) preconditions: tasks-scheduled( trs, ts) schedule-satisfactory( project, ts, ept, tas, ps ) { parallel: each (modify-design, mn, p, d) in ts, act-id == instantiate Modify-Design(mn) assign act-id to p schedule completion of act-id by d ta' == ta + (act-id, modify-design, mn) each (review-design-mods, mn, p, d) in ts, act-id == instantiate Review-Design(mn) assign act-id to { p | (review-design-mods,mn,p,d) in ts} schedule completion of act-id by d ta' == ta + (act-id, review-design-mods, mn) each (modify-code, mn, p, d) in ts, act-id == instantiate Modify-Code(mn) assign act-id to p schedule completion of act-id by d ta' == ta + (act-id, modify-code, mn) each (review-code-mods, mn, p, d) in ts, act-id == instantiate Review-Code(mn) assign act-id to { p | (review-code-mods,mn,p,d) in ts} schedule completion of act-id by d ta' == ta + (act-id, review-code-mods, mn) each (modify-mod-test-plans, mn, p, d) in ts, act-id == instantiate Modify-Module-Test-Plans(mn) assign act-id to p schedule completion of act-id by d ta' == ta + (act-id, modify-tests, mn) each (modify-sys-test-plans, sn, p, d) in ts, act-id == instantiate Modify-System-Test-Plans(sn) assign act-id to p schedule completion of act-id by d ta' == ta + (act-id, modify-harness, mn) each (review-mod-test-plans, mn, p, d) in ts, act-id == instantiate Review-Module-Test-Plans(mn) assign act-id to { p | (review-mod-test-plans,mn,p,d) in ts} schedule completion of act-id by d ta' == ta + (act-id, modify-design, mn) each (review-sys-test-plans, sn, p, d) in ts, act-id == instantiate Review-System-Test-Plans(mn) assign act-id to { p | (review-sys-test-plans,mn,p,d) in ts} schedule completion of act-id by d ta' == ta + (act-id, modify-design, mn) each (test-module, mn, p, d) in ts, act-id == instantiate Test-Module(mn) assign act-id to p schedule completion of act-id by d ta' == ta + (act-id, test-module, mn) each (test-system, sn, p, d) in ts, act-id == instantiate Test-System(mn) assign act-id to p schedule completion of act-id by d ta' == ta + (act-id, modify-design, mn) } 1. postconditions: tasks-assigned( ts, ta) personnel-notified-of-assignments(ts) obligations: activity Monitor-Tasks ( task-role-set trs, task-sched-set ts, task-assmnt-set ta, task-effort-set ept, time-avlble-set tas, project-span ps ) preconditions: tasks-assigned( ts, ta) personnel-notified-of-assignments(ts) { object events event-set object mod-tasks task-sched-set object new-tasks task-sched-set iterate: arbitrary: sequence: Monitor-Events( ts, events ) Reschedule-Tasks(trs,ts,ta,ept,tas,ps,events,mod-tasks,new-tasks) Assign-Tasks(trs,new-tasksts,ta,ept,tas,ps) Reassign-Tasks(trs,ts,ta,ept,tas,ps,mod-tasks) Merge-Schedules( mod-tasks, new-tasks, ts ) Suspend-and-Resume-Project() until system-modification-completed(new-reqs,mod-sys-design,mod-sys-source, mod-syshar,mod-stests,mod-modhars,mod-mtests) or ccb-cancellation( new-reqs ) } results: 1. postconditions: system-modification-completed(new-reqs,mod-sys-design,mod-sys-source, mod-syshar,mod-stests,mod-modhars,mod-mtests) obligations: 2. postconditions: ccb-cancellation( new-reqs ) obligations: activity Monitor-Events( task-sched-set ts, event-set events ) preconditions: { primitive } results: 1. postconditions: events != {} obligations: some task-sched-set mts, task-reassigned( mts, ta ) activity Reschedule-Tasks( task-role-set trs, task-sched-set ts, task-assmnt-set ta, task-effort-set ept, time-avlble-set tas, project-span ps, event-set events, task-sched-set modts, task-sched-set newts) -- modts is ts with whatever modifications are necessary -- newts is a set of new tasks not in either ts or modts preconditions: events != {} { primitive } results: 1. postconditions: modts - newts == 0 tasks-scheduled( trs, modts) tasks-scheduled( trs, newts) schedule-satisfactory( project, modts, ept, tas, ps ) schedule-satisfactory( project, newts, ept, tas, ps ) schedule-satisfactory( project, modts+newts, ept, tas, ps ) obligations: personnel-notified-of-reassignments( ts - modts, modts - ts ) personnel-notified-os-assignments( newts ) Activity Reassign-Tasks( task-role-set trs, task-sched-set ts, task-assmnt-set ta, task-effort-set ept, time-avlble-set tas, project-span ps, task-sched-set modts ) preconditions: tasks-scheduled( trs, modts) schedule-satisfactory( project, modts, ept, tas, ps ) { -- assumes that no activity is cancelled when rescheduling parallel: each (modify-design, mn, p, d) in modts - ts and (act-id, t, mn) in ta reassign act-id to p reschedule completion of act-id to d each (review-design-mods, mn, p, d) in modts - ts and (act-id, t, mn) in ta reassign act-id to { p | (review-design-mods,mn,p,d) in ts} reschedule completion of act-id to d each (modify-code, mn, p, d) in modts - ts and (act-id, t, mn) in ta reassign act-id to p reschedule completion of act-id to d each (review-code-mods, mn, p, d) in modts - ts and (act-id, t, mn) in ta reassign act-id to { p | (review-code-mods,mn,p,d) in ts} reschedule completion of act-id to d each (modify-mod-test-plans, mn, p, d) in modts - ts and (act-id, t, mn) in ta reassign act-id to p reschedule completion of act-id to d each (modify-sys-test-plans, sn, p, d) in modts - ts and (act-id, t, mn) in ta reassign act-id to p reschedule completion of act-id to d each (review-mod-test-plans, mn, p, d) in modts - ts and (act-id, t, mn) in ta reassign act-id to { p | (review-mod-test-plans,mn,p,d) in ts} schedule completion of act-id to d each (review-sys-test-plans, sn, p, d) in modts - ts and (act-id, t, mn) in ta reassign act-id to { p | (review-sys-test-plans,mn,p,d) in ts} reschedule completion of act-id to d each (test-module, mn, p, d) in modts - ts and (act-id, t, mn) in ta reassign act-id to p reschedule completion of act-id to d each (test-system, sn, p, d) in modts - ts and (act-id, t, mn) in ta reassign act-id to p reschedule completion of act-id to d } 1. postconditions: tasks-assigned( modts, ta) personnel-notified-of-reassignments( ts - modts, modts - ts ) obligations: activity Merge-Schedules( task-sched-set ts1, ts2, ts3 ) preconditions: schedule-satisfactory( project, ts1+ts2, , , , ) { primitive } results: 1. postconditions: ts3 == ts1 + ts2 obligations: activity Suspend-and-Resume-Project() preconditions: ccb-suspension(new-reqs) { primitive } results: 1. postconditions: ccb-resumption(new-reqs) obligations: 2. postconditions: ccb-cancellation(new-reqs) obligations: activity Modify-Design ( module-name mn ) let mod-sys-design == (sa, mds) preconditions: (modify-design, mn, SELF, d) in task-schedules { primitive } results: 1. postconditions: module-design-modified( mds[mn] ) requirements-satisfied( new-reqs, mds[mn] ) design-defects-remedied( {}, mds[mn] ) obligations: module-design-approved( review-team[mn], mds[mn]) activity Modify-Reviewed-Design ( module-name mn ) let mod-sys-design == (sa, mds) preconditions: (modify-design, mn, SELF, d) in task-schedules design-review-completed( new-reqs, mds[mn] ) module-defects[mn] != {} { primitive } results: 1. postconditions: module-design-modified( mds[mn] ) requirements-satisfied( new-reqs, mds[mn] ) design-defects-remedied( module-defects[mn], mds[mn] ) obligations: module-design-approved( review-team[mn], mds[mn]) activity Review-Design ( module-name mn ) let mod-sys-design == (sa, mds) preconditions: (review-design-mods, mn, SELF, d) in task-schedules requirements-satisfied( new-reqs, mds[mn] ) design-defects-remedied( module-defects[mn], mds[mn] ) { primitive } results: 1. postconditions: module-defects[mn] == {} requirements-satisfied( new-reqs, mds[mn] ) module-design-approved( review-team[mn], mds[mn]) module-design-review-completed( new-reqs, mds[mn] ) pm-notified-of-design-review( mn, TODAY ) obligations: module-source-modified( mod-sys-source[mn] ) 2. postconditions: module-defects[mn] != {} not requirements-satisfied( new-reqs, mds[mn] ) pm-notified-of-design-review( mn, TODAY ) obligations: requirements-satisfied( new-reqs, mds[mn] ) design-defects-remedied( module-defects[mn], mds[mn] ) activity Modify-Code ( module-name mn ) let mod-sys-design == (sa, mds) preconditions: (modify-code, mn, SELF, d) in task-schedules { primitive } results: 1. postconditions: module-source-modified( mod-sys-source[mn] ) design-satisfied( mds[mn], mod-sys-source[mn] ) compiled-errorfree( mod-sys-source[mn] ) module-defects[mn] == {} obligations: module-code-approved( reviewers, mod-sys-source[mn] ) 2. postconditions: module-interface-modified( mod-sys-source[mn] ) dependencies-determined( module-deps[mn] ) design-satisfied( mds[mn], mod-sys-source[mn] ) compiled-errorfree( mod-sys-source[mn] ) dependencies-notified-interface-change( module-deps[mn] ) obligations: module-interface-approved( reviewers, mod-sys-source[mn] ) activity Correct-Code ( module-name mn ) let mod-sys-design == (sa, mds) preconditions: (modify-code, mn, SELF, d) in task-schedules module-defects[mn] != {} { primitive } results: 1. postconditions: module-source-modified( mod-sys-source[mn] ) design-satisfied( mds[mn], mod-sys-source[mn] ) compiled-errorfree( mod-sys-source[mn] ) code-defects-remedied( module-defects[mn], mod-sys-source[mn] ) obligations: module-code-approved( reviewers, mod-sys-source[mn] ) 2. postconditions: module-interface-modified( mod-sys-source[mn] ) dependencies-determined( module-deps[mn] ) design-satisfied( mds[mn], mod-sys-source[mn] ) compiled-errorfree( mod-sys-source[mn] ) interface-defects-remedied( module-defects[mn], mod-sys-source[mn] ) dependencies-notified-interface-change( module-deps[mn] ) obligations: module-interface-approved( reviewers, mod-sys-source[mn] ) activity Review-Code ( module-name mn ) let mod-sys-design == (sa, mds) preconditions: (review-code, mn, SELF, d) in task-schedules code-defects-remedied( module-defects[mn], mod-sys-source[mn]) { primitive } results: 1. postconditions: module-defects[mn] == {} design-satisfied ( mds[mn], mod-sys-source[mn] ) module-code-approved( review-team[mn], mod-sys-source[mn] ) module-code-review-completed ( mds[mn], mod-sys-source[mn] ) pm-notified-of-code-review( mn, TODAY ) obligations: module-testing-completed( mod-mtests[mn] ) 2. postconditions: module-defects[mn] != {} not design-satisfied ( mds[mn], mod-sys-source[mn] ) pm-notified-of-code-review( mn, TODAY ) obligations: design-satisfied ( mds[mn], mod-sys-source[mn] ) code-defects-remedied( module-defects[mn], mod-sys-source[mn]) activity Review-Interface ( module-name mn ) let mod-sys-design == (sa, mds) preconditions: (depmod, SELF) in in module-owners and depmod in module-deps[mn] code-defects-remedied( module-defects[mn], mod-sys-source[mn]) { primitive } results: 1. postconditions: module-defects[mn] == {} design-satisfied ( mds[mn], mod-sys-source[mn] ) reviewers == { p | (depmod, p) in module-owners and depmod in module-deps[mn]} module-interface-approved( reviewers, mod-sys-source[mn] ) module-interface-review-completed ( mds[mn], mod-sys-source[mn] ) pm-notified-of-interface-review( mn, TODAY ) obligations: module-interfaces-consistent( mn, module-deps[mn] ) 2. postconditions: module-defects[mn] != {} not design-satisfied ( mds[mn], mod-sys-source[mn] ) pm-notified-of-interface-review( mn, TODAY ) obligations: design-satisfied ( mds[mn], mod-sys-source[mn] ) interface-defects-remedied( module-defects[mn], mod-sys-source[mn]) activity Modify-Module-Test-Plans ( module-name mn ) preconditions: (modify-mod-test-plans, mn, SELF, d) in task-schedules { primitive } results: 1. postconditions: module-tests-modified( mod-mtests[mn] ) covers( mod-mtests[mn], mod-sys-source[mn] ) module-harness-modified( mod-modhars[mn] ) test-defects-remedied({},mod-mtests[mn],mod-sys-source[mn]) obligations: module-testsuite-approved( review-teams[mn], mod-mtests[mn] ) module-testharness-approved ( review-teams[mn], mod-modhars[mn] ) activity Modify-Reviewed-Module-Test-Plans ( module-name mn ) preconditions: test-defects[mn] != {} (modify-mod-test-plans, mn, SELF, d) in task-schedules { primitive } results: 1. postconditions: module-tests-modified( mod-mtests[mn] ) covers( mod-mtests[mn], mod-sys-source[mn] ) module-harness-modified( mod-modhars[mn] ) test-defects-remedied(test-defects[mn],mod-mtests[mn],mod-sys-source[mn]) obligations: module-testsuite-approved( review-teams[mn], mod-mtests[mn] ) module-testharness-approved ( review-teams[mn], mod-modhars[mn] ) activity Review-Module-Test-Plans ( module-name mn ) let mod-sys-design == (sa, mds) preconditions: (review-mod-test-plans, mn, SELF, d) in task-schedules test-defects-remedied(test-defects[mn],mod-mtests[mn],mod-sys-source[mn]) { primitive } results: 1. postconditions: test-defects[mn] == {} module-test-suite-approved( review-team[mn], mod-mtests[mn] ) module-testharness-approved( review-team[mn], mod-modhars[mn] ) module-test-plan-review-completed ( new-reqs, mds[mn], mod-mtests[mn], mod-modhars[mn] ) pm-notified-of-module-test-plan-review( mn, TODAY ) obligations: 2. postconditions: test-defects[mn] != {} not module-test-suite-approved( review-team[mn], mod-mtests[mn] ) not module-testharness-approved( review-team[mn], mod-modhars[mn] ) pm-notified-of-module-test-plan-review( mn, TODAY ) obligations: test-defects-remedied(test-defects[mn],mod-mtests[mn],mod-sys-source[mn]) activity Test-Module ( module-name mn ) let mod-sys-design == (sa, mds) preconditions: (test-module, mn, SELF, d) in task-schedules compiled-errorfree( mod-sys-source[mn] ) compiled-errorfree( mod-modhars[mn] ) module-defects[mn] == {} test-defects[mn] == {} { primitive } results: 1. postconditions: module-testing-completed( mod-mtests[mn] ) module-defects[mn] == {} test-defects[mn] == {} pm-notified-of-module-tested( mn, TODAY ) obligations: 2. postconditions: module-defects[mn] != {} pm-notified-of-module-tested( mn, TODAY ) obligations: code-defects-remedied( module-defects[mn], mds[mn] ) 3. postconditions: test-defects[mn] != {} pm-notified-of-module-tested( mn, TODAY ) obligations: test-defects-remedied( test-defects[mn], mod-mtests[mn], mod-modhars[mn]) activity Modify-System-Test-Plans ( system-name sn ) preconditions: (modify-sys-test-plans, mn, SELF, d) in task-schedules { primitive } results: 1. postconditions: sys-tests-modified( mod-stests ) covers( mod-stests, mod-sys-source ) system-harness-modified( mod-syshars ) test-defects-remedied({},mod-stests,mod-syshars) obligations: system-testsuite-approved( review-teams[sn], mod-stests ) system-testharness-approved ( review-teams[sn], mod-syshars ) activity Modify-Reviewed-System-Test-Plans ( system-name sn ) preconditions: test-defects[sn] != {} (modify-sys-test-plans, sn, SELF, d) in task-schedules { primitive } results: 1. postconditions: system-tests-modified( mod-stests ) covers( mod-stests, mod-sys-source ) system-harness-modified( mod-syshars ) test-defects-remedied(test-defects[sn],mod-stests,mod-syshars) obligations: system-testsuite-approved( review-teams[sn], mod-stests ) system-testharness-approved ( review-teams[sn], mod-syshars ) activity Review-System-Test-Plans ( system-name sn ) preconditions: (review-sys-test-plans, mn, SELF, d) in task-schedules test-defects-remedied(test-defects[sn],mod-stests,mod-syshars) { primitive } results: 1. postconditions: test-defects[sn] == {} system-test-suite-approved( review-team[sn], mod-stests ) system-testharness-approved( review-team[sn], mod-syshars ) system-test-plan-review-completed ( new-reqs, mod-sys-design, mod-stests, mod-syshars ) pm-notified-of-system-test-plan-review( sn, TODAY ) obligations: 2. postconditions: test-defects[sn] != {} not system-test-suite-approved( review-team[sn], mod-stests ) not system-testharness-approved( review-team[sn], mod-syshars ) pm-notified-of-system-test-plan-review( sn, TODAY ) obligations: test-defects-remedied(test-defects[sn],mod-stests,mod-syshars) activity Test-System ( system-name sn ) preconditions: (test-system, mn, SELF, d) in task-schedules compiled-errorfree( mod-sys-source ) compiled-errorfree( mod-syshars] ) each module-name m, module-defects[m] == {} test-defects[sn] == {} { primitive } results: 1. postconditions: system-testing-completed( mod-stests ) each module-name m, module-defects[m] == {} test-defects[sn] == {} pm-notified-of-system-tested( sn, TODAY ) obligations: 2. postconditions: some module-name m, module-defects[m] != {} pm-notified-of-system-tested( sn, TODAY ) obligations: each module-name m, code-defects-remedied( module-defects[m], mod-sys-source[m] ) 3. postconditions: test-defects[sn] != {} pm-notified-of-system-tested( sn, TODAY ) obligations: test-defects-remedied( test-defects[sn], mod-stests, mod-syshars) initialization: act-id == instantiate Manage-Project() assign act-id to p in (p,project-manager) in project end Modify-System APPENDIX - ISPW7 Extensions 4.1 Teamwork 4.1.1 Resource Management See the example. The notion of duration is only present in the project organization model. The modeling language has only the notion of dates and time which have been used as deadlines and time-stamps for important events. 4.1.2 Coordination and Communication Concurrent activities are a basic part of the modeling approach. the degree of concurrency is constrained only by the assumptions and results of the activity descriptions. The dependencies among the preconditions, postconditions and obligations define a partial order on the activities. The coordination of interface changes has been expressed explicitly in the model. The natural form of interaction in Interact is that of asynchronous interaction. Synchronization is provided either by assigning a particular activity to a group (as is done in the reviewing process) or by scheduling a policy to be satisfied in a particular time frame (either explicitly as in the example, or through Intermediate by scheduling it dynamically). 4.1.3 IWSP6 Extensions Incorporated into the model. 4.2 Process Change 4.2.1 Process Modification the currently enacting process model may be modified by introducing a variant of the model that incorporates the change desired. In this case it would be a modification to the Modify-Code activity with the addition of the policy ``module-design-approved( review-team[mn], mds[mn])''. Model Modify-System-A specializes Model Modify-System activity Modify-Code ( module-name mn ) let mod-sys-design == (sa, mds) preconditions: (modify-code, mn, SELF, d) in task-schedules module-design-approved( review-team[mn], mds[mn]) { primitive } results: 1. postconditions: module-source-modified( mod-sys-source[mn] ) design-satisfied( mds[mn], mod-sys-source[mn] ) compiled-errorfree( mod-sys-source[mn] ) code-defects-remedied( {}, mod-sys-source[mn] ) obligations: module-code-approved( reviewers, mod-sys-source[mn] ) 2. postconditions: module-interface-modified( mod-sys-source[mn] ) dependencies-determined( module-deps[mn] ) design-satisfied( mds[mn], mod-sys-source[mn] ) compiled-errorfree( mod-sys-source[mn] ) interface-defects-remedied( module-defects[mn], mod-sys-source[mn] ) dependencies-notified-interface-change( module-deps[mn] ) obligations: module-interface-approved( reviewers, mod-sys-source[mn] ) End Modify-System-A Another possible approach would have been to define a policy ``coding-permissible'' that could then have several definitions, one of which would require the approval of the design, and one which would not. The problem of consistency is one that requires an administrative decision. There are however, several problems: first, it is possible for a precondition to become false after the initiation of an activity; second, it may become false before the start of an activity. The administrator must decide who the new description is to be enforced, mindful of the potential problems enumerated above. Intermediate allows the administrator to allow inconsistencies with currently` enacting processes or to require their rollback. 4.2.2 Process Exceptions Intermediate provides two ways to handle exceptions: to define several results, some of which may be exceptions; and to modify the existing description to handle the unexpected circumstances. The latter may be done by altering a policy definition or an activity description. In the following example, similar to the one above, we add another result that does not require a review of the design changes but requires only that the code be modified as a result fo the redesign. Model Modify-System-B specializes Model Modify-System activity Modify-Reviewed-Design ( module-name mn ) let mod-sys-design == (sa, mds) preconditions: (modify-design, mn, SELF, d) in task-schedules design-review-completed( new-reqs, mds[mn] ) module-defects[mn] != {} { primitive } results: 1. postconditions: module-design-modified( mds[mn] ) requirements-satisfied( new-reqs, mds[mn] ) design-defects-remedied( module-defects[mn], mds[mn] ) obligations: module-design-approved( review-team[mn], mds[mn]) 2. postconditions: module-design-modified( mds[mn] ) requirements-satisfied( new-reqs, mds[mn] ) design-defects-remedied( module-defects[mn], mds[mn] ) obligations: module-source-modified( mod-sys-source[mn] ) End Modify-System-B