Afgeronde rechthoek: Top of book Afgeronde rechthoek: Managers track Afgeronde rechthoek: Technical track Afgeronde rechthoek: Previous page Afgeronde rechthoek: Home
 

 

 

 


Page contents

The structure of formal specification document repositories. 36

Establishing standardized exchange of specification documents  37

Implementation. 48

Restrictions. 52

Reusable items. 54

Integrity. 57

Integrity of the repository structure. 58

Integrity of formal specification document identity. 64

The standard. 69

General structure. 73

The formal specification documents. 74

The necessary and the optional items in a formal specification document 76

Types of formal specification documents. 87

XML Restrictions. 116

Example. 118

XMI 120

Stores of types of formal specification documents. 132

Dedicated repositories. 135

Fixed node names. 139

Relative addressing. 153

Navigation. 155

Categorization. 160

Completing the picture. 166

Document editors. 167

The formal specification document importer 172

The formal specification document exporter 175

Proof of concept 179

Editor/viewers. 185

Document exporter 188

Document importer 190

Other tools. 192

Conclusion. 194

 

The structure of formal specification document repositories

Establishing standardized exchange of specification documents

If formal specification documents can be exchanged in a standardized way and can be inspected on public accessible repositories that also offer the opportunity to download these documents, then one of the most essential requirements for establishing an open exchange of formal specification documents is fulfilled.

The main problems that occur when information on subjects must be exchanged between independent parties that need not have initial knowledge of each other are:

·        Where can the client find the information?

·        How can the client query the information base for items that are of interest to him?

·        What protocol is available for information exchange?

·        How can the information be interpreted?

·        Can the client choose freely between manual and automatic information access?

The advent of XML and XML related utilities has brought standardized ways for resolving these problems. This is exploited in the described implementation of a series of repositories that contain formal specification documents.

A web or locally based repository for formal specification documents is described that has the structure of a directory tree. For a part, that directory tree is strictly defined. Some of the files in this directory have a predetermined content structure. This content defines the navigation and categorization capabilities of a part of the repository. Other files define the general structure of formal specification documents for a series of types of formal specification documents. The technology used, is based on internationally accepted standards and the technology is platform independent. The more or less fixed files are XML files or XML Schema files and enable independent tool vendors to build dedicated tools that make use of this structure. Dedicated tools are capable of analyzing the XML schema files and use the result to offer the operator the capability to generate new instances of the formal specification documents. Other tools enable interactive editing of new and existing instances of the corresponding formal specification document type. The same or another tool may be used to store the finalized formal specification documents onto one ore more target repositories. Tools exist that enable the interactive generation of new document types that will be stored in corresponding XML schema files. Special import tools support browsing of the existing repositories for predetermined subject categories of formal specification documents and download the search results into a local repository, where other tools can use these documents.

Repositories fall into two categories. For establishing their navigation and categorization integrity, the passive repositories depend on export tools that put the locally prepared repository on its final location. Active repositories can interactively accept additions and independently keep the navigation and categorization integrity. The addition of new documents or new document types is done via web-services. Depending on the capabilities of the web-service, a complete sub-tree that contains documents, document types and promotion pages can be added to the repository.

Implementation

The technology used in this approach is platform independent and is based on internationally accepted standards. The files and utilities used are HTML or XML files and files and utilities that support these file types. All of the involved standards can be found on http://www.w3.org.

The formal specification document repository offers navigation possibilities for both humans and automates. It also offers categorization for the formal specification documents that are contained in the directory tree. Again this is implemented such, that it is accessible both by humans and by automates. Human access is supported by HTML technology. Computerized access is offered via XML technology.

This specification only defines the bare structure of the repository. An actual repository may be decorated with means that give a more appealing outlook. The formal specification document repository may also contain other kinds of documents, but these documents do not play an essential role in the structure and functionality of the repository. For example at several places explanatory or promotional documents may be placed. Another possibility is to offer more efficient download purposes, such as a compressed file that contains the contents of a sub-tree in the node that contains this sub-tree. As a rule, virtual HTML access that is humanly consumable is offered by XSLT transformation of XML documents in virtual HTML pages. Not all browsers support XSLT transformations. However, most modern browsers will perform this task properly.

Restrictions

All relevant file names and directory names in the formal specification document repository are lower case. The repositories as well as the contained formal specification documents have a purely hierarchical structure. There are no links within documents. However, documents may contain links to other documents. These links may have a complex nature. For example if a specification document of a component class uses a series of interfaces, then it can combine the reference to the interface specification document with a series of values that represent initialization values for the target. Restricting to a purely hierarchical eases the navigation within repositories and simplifies the maintainability of the repositories and of the contained documents. Due to this restriction, only a subcategory of XML files will validate as proper formal specification documents.

Reusable items

The proposed repository puts all reusable items in separate documents. The client documents that want to use these items may refer to these documents. It is possible to give the reusable documents a more general nature and let the clients set some of the attributes of the item before using it.

For example, the name and the alias of a more generally reusable data type can be set before using it. The software application that uses these documents may construct a ‘typedef’ for the name ‘DWORD’ by using the alias ’unsigned long’: “typedef DWORD unsigned long”.

Integrity

Integrity of the repository structure

Formal specification document repositories may reside

·        On the Internet, where they are publicly accessible

·        On the Intranet or locally on a LAN file system

·        On the hard disk of the document creator/editor.

In the latter cases, the formal specification document repository is only accessible to a closed community. Sub-trees of a repository may be copied or moved to another formal specification document repository, but in any case the integrity of the structure of the involved repository must be kept intact. An active formal specification document repository may be capable of keeping its own navigation and categorization integrity intact. For other formal specification document repositories, this means that only trustable tools may alter the content of the repository.

Integrity of formal specification document identity

Whenever a formal specification document is published on a formal specification document repository, whether locally or on the web, the contents of that document are forever fixed. This means that whenever the content of a document is altered, its formal specification document must be replaced by a formal specification document with a different identity. Two or more identifiers set the identity of a formal specification document:

1.      The name of the document. This name is used for naming the file in which the formal specification document will be stored and for the name of the directory that contains the document file.

2.      An URI that locates the originator of the formal specification document. This is the location where the formal specification document is, was, or will be published for the first time in a publicly accessible formal specification document repository.

3.      An optional globally unique identifier (GUID). This identifier may be used by applications that make use of the formal specification document.

The standard

In order to make the repositories accessible by a large category of users they must obey a standard. The standard defines the structure of the directory trees, the general structure of the supported XML files and the format and structure of the navigation and categorization utilities. This standard is also supported by reference repositories. A reference repository represents a publicly accessible internationally formal specification document exchange standard for a specific domain. A reference repository for a given domain may appear at multiple locations. In that case, these reference repositories must be identical.

A reference repository contains, in the form of XML Schemas, the internationally accepted specifications of the general structure of types of formal specification documents for the corresponding domain. Further, it contains XML Schema files that specify the general structure of the files that implement the navigation and categorization functionality of standardized formal specification document repositories. A reference repository may contain samples of formal specification documents that can be used for educational or for referential purposes.

The XML Schema files that are located at several locations in the formal specification document repository correspond to identical XML Schema files in the reference repository. Together with the structure of the directory tree as is specified in table 2, these files define the structure, the functionality and the restrictions of the formal specification document repository. The repositories use a subset of the capabilities of XML. In this way, it becomes relatively easy to create sets of adaptive tools that can work properly for each formal specification document in each of these formal specification document repositories. It also enables independent tool vendors to develop dedicated tools that target sections of a formal specification document repository where given types of documents are stored.

General structure

The formal specification documents

All formal specification documents are located at a leaf of the directory tree. Each leaf of the directory tree is devoted to only one formal specification document. The name of the directory corresponds with the name of the document. In addition, the name of the file that contains the formal specification document must correspond with the name of the formal specification document. The extension of that file may be “.xml” or it may correspond to the namespace prefix of the namespace that rules the formal specification document. This namespace is defined in an XML Schema file that is located at a node one level up in the directory tree. This node is devoted to a type of formal specification documents. These types describe a given group of formal specification documents in a general sense. If a reference repository exists for this domain, then an identical XML Schema file must exist at a similar location in the reference repository. The namespace-URI of the formal specification document refers to the name of the type category. The namespace string is constructed as “nameoftypecategory_schema”. In this example, ‘nameoftypecategory’ stands for the actual name of the type category. A sample file name for a formal specification document is “mypackage.pkg”. The extension “.pkg” corresponds to the namespace prefix of the reusable formal specification document element type “package”. A namespace is unique, but a namespace prefix need not be unique. Care must be taken that this does not raise conflicts.

The necessary and the optional items in a formal specification document

In this context, formal specification documents are XML documents. All formal specification documents must refer to the XML Schema that defines their namespace. In the formal specification document repository the namespace URI of the formal specification documents corresponds with the name of the type category that governs this namespace. It is constructed as “nameoftypecategory_schema”. The local name of the top element corresponds with the name of the formal specification document type category.

Optionally a formal specification document may contain a reference to an XSL document that is used to render the document in a format that is better suited for human interpretation.

All formal specification documents must contain in their top element a string type attribute with name ‘Name’ that contains the name of the document. All formal specification documents must also refer to the location of their originator. Specifying in the top element an attribute with name ‘Originator’ that contains the URI where the document is, was or will be published for the first time on a publicly accessible formal specification document repository does this. An optional string type attribute with name ‘MyGuid’ may contain a globally unique identifier (GUID). Further, the top element of a formal specification document type may contain any kind of additional attributes. Attributes that have a value that equals the default value of that attribute will usually not appear in the document.

In order to indicate that a document is not yet finalized, the top element of a formal specification document may contain a Boolean attribute with name “Final” that has its value set to ‘false’. The default value of the “Final” attribute is ‘true’. Documents with this value set to ‘false’ can never appear on a published formal specification document repository. However, these documents can be temporary working documents of document editors. They might appear in a local workspace that has a structure, which closely resembles a formal specification document repository. In this way, a set of finalized documents and documents that are not yet finalized can be kept in proper order.

A top element of a formal specification document, or its child elements, may contain a series of necessarily present child elements. If the element has a name, then a string attribute with name ‘Name’ must contain that value. If the element has a property that is an URI location, then that property must be held by an attribute that has the name ‘Location’.

Further, a formal specification document or its child elements may contain lists of optional elements. The optional elements in a list are child of a surrounding list element. If the list is empty, the surrounding list element does not appear in the document. An element may contain zero or more of these list containers.

Backup locations

Zero or more backup locations may be specified in a special list element that is child of the top element. The local name of such elements is ‘BackupLocation’. The element contains an attribute with name ‘Location’ that contains the URI to the backup location. The group of backup location elements is contained in a list element that has ‘BackupLocations’ as its local name. If the list is empty, the ‘BackupLocations’ element does not appear in the document. Other than top elements may also contain lists of backup locations. The same naming convention must be used for these lists.

Categories

Zero or more subject categories may be specified in a special list element with name ‘Categories’ that is child of the top element. The local name of such elements is ‘Category’. The element contains an attribute with name ‘Name’ that contains the name of the subject category. Another string attribute, named “OwnerType”, contains the name of the type of the document that owns this list of categories. A string attribute with name “OwnerPath” contains the pathname of the directory that contains the owner. A string attribute with name “OwnerFileName” contains the file name of the owner. An URI attribute with name “DescriptionLocation” contains the location of an informal description of this category. The group of ‘category’ elements is contained in a list element that has ‘Categories’ as its local name. If the list is empty, the ‘Categories’ element does not appear in the document. When the document is saved, the toolkit creates a separate file with name “categories.xml” that contains the categories list as the top element. Document export tools and active repositories use these extra files in order to create the categorization utilities of the repository.

Types of formal specification documents

The following table contains guidelines for defining new types of formal specification documents. If ‘Optional’ is indicated, this does not mean that the item is optional in the target document specification. In a given document-type specification, the presence can be either ‘Optional’ or ‘Necessary’.

 

 

Item

Type of item

Name

Appearance

Presence

NamespaceURI

namespaceURI

Derived from the name of the type category

Top element

Necessary

XSL reference

 

n.a

Top element

Optional

Local name

string

Equal to the name of the type category

Top element

Necessary

Prefix

string

Equal to the namespace prefix of the type category

Top element

Necessary

Attribute

string

‘Name’

Top element

Necessary

Attribute

string

‘Name’

Child element

Optional

Attribute

URI

‘Originator’

Top element

Necessary

Attribute

URI

‘Location’

Any element

Optional

Attribute

string

‘MyGuid’

Top element

Optional

Attribute

boolean, default=’true’

‘Final’

Top element

Optional

Attribute

Enum type defined as a simpleType

Any name that is unique in the element

Any element

Optional

Attribute

Any type

Any name that is unique in the element

Any element

Optional

Element

complexType

Name of the document type category

Is top element

Necessary

Element

List element (complexType)

Not prescribed

Any element. Does not appear when list is empty

Optional

Element

Child element (complexType)

Not prescribed

Any element

Optional

Element

List element (complexType)

‘BackupLocations’

Any element Does not appear when list is empty

Optional

Element

Child element of ‘BackupLocations’ Has a ‘Location’ attribute

‘BackupLocation’

Child of ‘BackupLocations’

Optional

Element

List element (complexType)

‘Categories’

Top element.   Does not appear when list is empty

Optional

Element

Child element of ‘Categories’ Has a ‘Name’ attribute

‘Category’

Child of ‘Categories’

Optional

Element

Reference element Has a ‘Location’ attribute

Not prescribed

Child of any element or member of list

Optional

 

 

Formal specification documents are categorized into type categories. A corresponding XML Schema file specifies each type category. This file defines the namespace of that type and is also specifies a namespace prefix that is unique within the repository. Apart from that, each category type has a name. This name is also unique within the domain of the repository.

The nodes that are devoted to the type categories of formal specification documents are located one level above the leaf elements of the directory tree. The name of that directory corresponds with the name of the type category. The sub-tree that belongs to this node only contains formal specification documents that belong to this type category. A sample path to a formal specification document starting at the node of the package type category is “package/mypackage/mypackage.pkg”. The corresponding XML Schema file has the name “package.xsd” and is located in the ‘package’ directory.

XML Restrictions

In order to simplify the analysis of the formal specification document types, some restrictions are posed on the document types that will conform to the proposed standard. A conforming formal specification document is an XML document that contains elements in the form of complex types. These complex types may contain a set of optional complex types that are contained in a surrounding complex type. That surrounding container element must not contain any compulsory elements. Its child elements must be contained in a ‘choice’ section. If this list-container is empty, it will not appear in the XML document. The list-container may accept child elements that belong to a small set of element types. The list-container must not have any attributes. An element may contain zero or more of these list-containers. Any element may contain zero or more list-containers. All elements, except list-containers, may contain zero or more compulsory elements. These compulsory child elements must be contained in an ‘all’ section. All elements may contain zero or more attributes. The types of these attributes must be standard XML data types. However, enum types may be defined via a simple type.

Example

An example instance of the proposed repository is ExampleRepository. This is a very bare implementation. Little is done to give the repository a more appetizing look and feel. Adding more sophisticated XSLT transformation utilities may accomplish this.

XMI

The produced documents are intentionally not XMI compatible. However if an outer XML element was added with name ‘XMI’ and with namespace ‘xmlns:xmi=”http://www.omg.org/XMI” ‘, then the document would be fully XMI compliant. Thus, it is easy to convert the documents into XMI compliant documents. Nevertheless, the approach taken in the proposed repository standard differs for the following reasons:

·        The internals of the document do not contain internal references that would oblige identifiers such as the xmi:id attribute. Reusable items are put in separate documents and are referenced from the client document

·        A single element may refer to several external documents

·        References make use of relative addressing, a mechanism that is specific to this repository standard

·        No typical XMI elements are used or would be required

·        No typical XMI attributes are used or would be required

·        XMI offers many options that would make the build of a generally applicable parser a burden

·        The proposed repository sets restrictions that would tolerate only a very small subset of XMI documents

·        The restrictions still offer sufficient flexibility to allow making all possible specification documents comply with them.

Thus, making the documents XMI compatible would add no additional advantages and can only introduce confusion and unwanted complexity.

For more information on XMI, please see http://www.omg.org/technology/xml, or read the book “Mastering XMI” by T. J. Grose, G.C. Doney and S.A. Brodsky.

Stores of types of formal specification documents

Reusables-stores contain formal specification documents that for some reason are set apart. Directory tree nodes, named ‘reusablesstore’ and located at three levels above the leafs of the directory tree contain the sub-trees that are devoted to dedicated reusables-stores. The root of these sub-trees may contain a document that explains why the formal specification documents are set apart. A reason may be that all these documents are devoted to a given subject category or to a coherent group of subject categories. Another reason may be that the documents originate from the same creator or the same company.

A sample path from the reusables-store node to a formal specification document is: “reusablesstore/reusablesofmycompany/package/mypackage/mypackage.pkg”.

Dedicated repositories

Parts of a repository may be dedicated to a certain purpose. The root of the repository contains sub-trees that contain dedicated repository parts. The root of these sub-trees may contain a document that explains why the formal specification documents in this dedicated repository are set apart. One of the reasons may be that the dedicated repository is used to store types of formal specification documents or complete reusables-stores that are retrieved from other repositories.

A sample path from the repository root to a formal specification document is: “repository/local_repository/../../../reusablesstore/reusablesofmycompany/package/theirpackage/theirpackage.pkg”.

Another sample is: “repository/mycompaniesrepository/../../../reusablesstore/reusablesofmycompany/package/mypackage/mypackage.pkg”.

Fixed node names

The number of levels in a path from root to leaf is not fixed. It must be 5 or higher. At some levels, the repository nodes have fixed or defined directory names.

 

Level

Directory name

top

repository

top-1

The directory name is not fixed

The directory name is not fixed

The directory name is not fixed

3

reusablesstore

2

The directory name is not fixed

1

The directory name equals the name of the type category

0

The directory name equals the name of the formal specification document

 

The file containing the formal specification document has a filename corresponding to the name of the formal specification document and an extension that is “.xml” or that corresponds to the namespace prefix of the namespace of the formal specification document. The NamespaceURI, the LocalName and the Prefix of the top element must correspond with the type category that is defined in level 1

 

Relative addressing

The fixed node names ‘repository’ and ‘reusablessstore’ are used for relative addressing. Relative addressing is used to cope with the burden of adapting references to external documents, when a repository or part of a repository is moved to another location. Relative addressing makes use of a fixed prefix ‘http://www.the_origin_substitute.none’. This part of a non-existing URL is used to render the relative address again as a valid URI. If the location of a formal specification document is given by: “E:/design_area/repository/local_repository/Johns_stuff/reusablesstore/reusablesofmycompany/package/mypackage/mypackage.pkg”, then the toolkit or the application that makes use of the document will convert the relative address “http://www.the_origin_substitute.none/reusablesstore/reusablesofmycompany/interface/myinterface/myinterface.pkg” to the absolute address “E:/design_area/repository/local_repository/Johns_stuff/reusablesstore/reusablesofmycompany/interface/myinterface/myinterface.pkg”.

Navigation

Each node in the directory tree contains a “default.html” document. This document links to the local “default.xml” file. That file uses an XSLT transformation to construct a virtual html file that contains hyperlinks to all relevant documents in the corresponding sub-tree. The XSLT transformation file is located at the root of the repository and its name is “mydefault.xsl”. Higher-level virtual “default.html” documents will link to lower-level “default.xml” documents and indirectly to lower-level virtual “default.html” documents. Usually the Internet browser selects the local “default.html” document when an URI to the directory without a file name is offered as an address.

Each node in the directory tree contains a “default.xml” document. This document contains references to all relevant documents in the corresponding sub-tree. Humans more easily navigate by using the actual or virtual  “default.html” documents, but automates can more easily work with XML documents than with HTML documents. Thus, dedicated automatic navigators will most likely use the “default.xml” documents to traverse the directory tree.

An XML Schema file located in the root of the repository specifies the general structure of the “default.xml” documents. Its name is “default.xsd”. This file is a copy of the “default.xsd” that is located at the root of the reference repository.

After addition or removal of files or directory sub-trees an appropriate active formal specification document repository will be capable of keeping the content of the navigation files in correspondence with the contents of the repository.

Categorization

Each node in the directory tree contains a “categories.html” document. This document links to the local “categories.xml” file. That file uses an XSLT transformation to construct a virtual html file that represents a virtual “categories.html” document. The XSLT transformation file is located at the root of the repository and its name is “mycategories.xsl”. The virtual document enumerates the subject categories that are targeted by the formal specification documents that are contained in the corresponding directory sub-tree. A list of hyperlinks to the corresponding directory tree leafs is attached to each of the enumerated categories. This list will be subdivided in sections that correspond to a reusable formal specification document element type. If the category has a description, then this is indicated at the line where the category name is listed. A formal specification document may target zero or more subject categories. Thus, formal specification documents need not have any categories. The leaf elements of the repository contain a “categories.xml” file that has a different structure. This file does not support the XSLT transformation that is contained in the “mycategories.xsl” file.

Each node in the directory tree contains a “categories.xml” document. Except for the “categories.xml” documents in the leaf elements of the repository, these documents enumerate the subject categories that are targeted by the formal specification documents that are contained in the corresponding directory sub-tree. The file may be empty. The category elements contain the name of the category, the type name of the owner-document, the path to the leaf that contains the owner, the file name of the owner and the location of the description of the category. The list of categories is sorted with respect to category names, owner document type names and owner paths.

Humans more easily work with the virtual “categories.html” documents, but automates can more easily work with XML documents than with HTML documents. Thus, computerized categorization utilities will most likely use the “category.xml” documents to search the directory tree for relevant documents.

An XML Schema file located in the root of the repository specifies the general structure of the “categories.xml” documents. Its name is “categories.xsd”. This file is a copy of the “categories.xsd” that is located at the root of the reference repository.

After addition or removal of files or directory sub-trees, an appropriate active formal specification document repository will be capable of keeping the content of the categorization files in correspondence with the contents of the repository.

Completing the picture

Document editors

Document editors that make use of formal specification document repositories must be able to create and edit formal specification documents in accordance with the XML Schema files that define the namespace of that document. These XML Schema files reside at the type category nodes of the formal specification document repository, one level above the leaf elements of the directory tree. Sophisticated document editors, or toolkits that contain such editors, may be able to create the XML Schema files and the complete structure of the corresponding sub-tree of a target formal specification document repository or reusables-store.

When a new document is created, it might be stored locally in a directory tree. The structure of that directory is a replica of a sub-tree of a formal specification document repository. However, the strict rules of the formal specification document repository do not hold for this directory tree. For example, the navigation and categorization mechanism may be missing. In addition, the files may be read-write files rather than read-only files. Moreover, there is no restriction on the change of a formal specification document specification.

Often formal specification documents contain references to other formal specification documents. For that reason, the document editor may make use of a local formal specification document repository that contains locally created formal specification documents and formal specification documents that are retrieved from other repositories. The retrieved files in this repository are read-only. In addition, the results of the document editor may be stored in this local repository. After each add or removal, the integrity of the structure of the local formal specification document repository may be re-ensured. This is normally done by another tool, the document exporter. Retrieving formal specification documents from other formal specification document repositories is the task of the formal specification document import tool.

The designer that operates the document editor may decide to finalize a given specification document. After finalization, the document may be exported to one or more publicly accessible target repositories. It is possible that the original document contains elements that must not be published. These elements must contain a Boolean attribute that is named HideFromPublication. The default value for that attribute is ‘false’. When set ‘true’ the stored finalized specification document will no longer contain that element. In order not to lose information in this way, the prepare-for-export function of the editor tool will usually store specification documents in an intermediate location. The export tool will use this intermediate location as its source.

The formal specification document importer

The formal specification document import tool searches one or more formal specification document repositories and downloads types of formal specification documents that correspond to the target subject categories of the client document editor. The downloaded items are placed in a local area that is a replica of a formal specification document repository. The document exporter tool may be used to keep the integrity of the local workspace intact.

The operator that uses the document import tool may differ from the user of the document editing-tool that is going to use the imported information.

The formal specification document exporter

When a formal specification document is prepared for export, it will be placed in a directory tree that will be copied to a formal specification document repository. This deployment action is the task of a formal specification document export tool. The document editors have facilities for the creation and interpretation of relative addresses. The document export tool may also convert absolute (local) addresses to relative addresses. An important task of the document exporter is the establishment of the navigation and categorization integrity of the local repository before it is exported. Formal specification document export utilities start from a local directory tree and transform that directory such that the structure of the directory tree and the files contained in it conform to the rules that hold for formal specification document repositories. When this is accomplished, the directory tree can be copied or moved to the target node of one or more target formal specification document repositories. It is possible to use the reordering functionality without exporting the whole or a part of the treated repository. It can be sensible to apply this capability to the local workspace.

If the target formal specification document repository is not capable of establishing its own integrity, then the formal specification document export tool must replace the complete repository. Otherwise, it is possible to export only a sub-tree of the local repository. Exporting a complete repository is only allowed when the operator of the formal specification document exporter is the owner of the target formal specification document repository. Exporting a sub-tree can be done via the intermediation of a suitable web-service.

In many cases a group of document editor operators work on the formal specification documents of a given directory sub-tree. For that reason the operator of the document exporter will then differ from the editor of the involved documents.

Proof of concept

In order to proof the feasibility of the proposed concepts, a prototype toolkit has been built that is capable of generating and maintaining a series of repositories that obey the proposed structure. The toolkit contains the following members:

·        Editor/viewers

·        Document exporter

·        Document importer

·        System composer

Editor/viewers

Two editor viewers exist, that can generate and edit types of formal specification documents and instances of formal specification document types. They can also be used to view existing instances of formal specification documents. The first tool, ‘UniFormer’, does exactly this. The second tool ‘Componector’, has the same functionality as ‘UniFormer’. Further, it makes use of a series of build-in types of formal specification documents. These types are all concerned with the formal specification of software components and with the formal specification of component based systems.

It is possible to devote dedicated editor/viewers to a given sub-category of types of formal specification documents. For example, it would be sensible to create an interactive graphical tool that helps creating, editing and viewing state-charts. The generated formal specification documents can then be published on the appropriate location of a formal specification document repository. Such tools are not yet built, but their feasibility is obvious. ‘Componector’ already implements a series of dedicated services that help establishing the mutual consistency of specification documents that play a role in a project that builds a component based system.

Document exporter

A tool, named ‘DocumentExporter’, is created that is able to transfer a project-directory-tree that has been filled with formal specification documents by ‘UniFormer” or “Componector’ or another compatible editor/viewer, to a local repository that obeys the proposed rules. A standard FTP tool can then transfer this local repository to a remote web site.

Document importer

A tool, named ‘DocumentBrowser’, can browse locally or remotely located repositories and load selected sub-trees of these repositories into a local directory tree. Usually this directory tree will be part of a local repository. The document loader can cooperate with the document exporter to keep the navigation and categorization integrity of the target repository intact. The tool ‘DocumentBrowser’ also plays the role of a category manager. This means that it can collect categories and names of formal specification document types from a series of repositories. A subset of these collections can then be used to download formal specification documents that belong to a given subset of categories and to a given subset of formal specification document types.

Other tools

Other tools make use of the formal specification documents. In case of documents that formally specify software components, such a tool may generate the source code of the skeletons of the software components that correspond to the specifications. Another tool or the same tool can use these skeletons and the formal specification of a component based system to create a working prototype of that system. The demo tool, named ‘CompoBuilder’, integrates the tasks of component skeleton generation, the automatic addition of a tailored infrastructure and the integration of these ingredients into a working and testable prototype. The tool establishes the proof of the feasibility of component based system generation from formal specification documents.

Conclusion

The proposed repository structure is feasible and can be supported by a toolkit that can perform its task independent of the type of formal specification document. The methodology works equally well for specifying the configuration of cars as for the specification of software modules or the specification of the widgets in a graphical user interface. The proposed repository delivers a flexible fundament on which a large series of dedicated tools can be built. This includes specialized or general-purpose editor/viewers, dedicated document browsers and tools that make use of the formal specification documents.

The original target of the proposed repository standard is the creation of an open market for software components in the domain of resource-restricted real-time embedded systems. For that purpose, a series of publicly accessible repositories must be available where formal specifications of software components can be published and retrieved. The proposed repository surpasses this aim in that it accepts any kind of formal specification document that fulfils the restrictions set by the proposal. The restrictions are minimal. Any formal specification document type can be made to comply with these restrictions.

 

 

Afgeronde rechthoek: Top of page Afgeronde rechthoek: Next page Tech Afgeronde rechthoek: Managers track