Example: Specification Modules

Suppose a team of four authors develops a software specification using the specification modules by sd&m. You find a comprehensive description of this example in Part III of my PhD thesis.

The specification consists of 18 documents: four specification documents (we have four reader species), one goals, scope, constraints document, one glossary, one reading instruction, one cross-cutting concerns document, three business processes (in three business process documents), ten use cases (in three use case documents), twelve analysis functions (in one analysis functions document), two dialogs (in one dialogs document), one data model, and one data types document. The specified system is subdivided into three components. We assume that the specification is developed by Maggie (project leader), Bob, Elli, and Peter, who perform 24 check-ins to the repository. You find a short repository change log here.

We have defined the following consistency rules:

1. goalsscope_one:
   There exists at most one valid goals, scope, constraints document.
2. overview_actors_unique:
   The name of an actor is unique and should comply with its naming convention in the cross-cutting concerns.
3. ccc_style_exists:
   The cross-cutting concerns of the fine specification should contain a style guide.
4. uc_unique:
   The name of a use case is unique and should comply with its naming convention in the cross-cutting concerns.
5. uc_preconditions:
   The preconditions of a use case should be satisfiable from the postconditions of all other use cases.
6. anafun_postcons_uc:
   The conjunction of the postconditions of all analysis functions referenced by a use case u should imply the postconditions of u.
7. dm_relation_cardinalities:
   In the finished fine specification, each relation should have cardinalities associated with its entity types.
8. dt_type_range:
   The lower bound of a range data type should be smaller than its upper bound.
9. dialog_anafun_uc:
   Each analysis function used by a dialog should also be used by each use case associated with this dialog.
10. glossary_invariant:
    The definition of a term in the glossary does not change significantly over time.
11. component_usecase_anafun:
    A use case should use analysis functions from its own component only.
12. component_entitytypesrelations:
    In the data model, an entity type has more relations to entity types within the same component than to entity types within a different component.
13. spec_bp_notlost:
    A system-supported activity in a business process of the coarse specification is also included in the fine specification and is also supported by the system.
14. spec_readers:
    A specification intended for a species of readers only contains documents intended for this reader species.
15. doc_inprogress_qualityassurance:
    A document in status `in progress' should change its status to `quality assurance' only.

At each repository state, CDET generates fifteen S-DAGs (one for each rule) and one repair collection. You find S-DAGs and repair collections here.

For this example we need the following technical ingredients:

• The XML project description file skischool/xml/SDM_Check.xml, which is specific to this project.
• The rules, which may be used for all projects using the specification modules (and here the XML rule definition file xml/SDM_Rules.xml)
• The domain specific language, which may be used for all projects using the specification modules (and here the XML language definition file xml/SDMLanguage.xml)
• Parsers imported by our language. Unfortunately, we have to do a bit of hand work here because the parsers generated by HaXml from the specification modules DTDs ignore subtypes.

Last modified: Mon Jan 31 17:02:09 CET 2005