Measuring Attributes of Concurrent Software Specifications in Petri Nets

Specifications play a crucial role in the development of many types of software systems. Formal specification techniques are often used to help ensure that the requirements are correctly captured and to prove or check properties of the developed software. This is especially true in systems such as concurrent software systems, due to the critical nature that such systems may have. Though the growing importance of the specification phase shows the emerging need for extending measurement to it, few measures have been defined for specifications. The main reason is that specifications have often been written in informal languages, which made it hard to define and collect measures for software specifications. Instead, formal specifications would have a great potential for being measured. This paper proposes a set of measures for capturing a number of internal attributes (i.e., size, length, complexity, and coupling) of software specifications written with Petri nets, a well-known formal technique for modeling concurrent systems. These measures are theoretically validated against a collection of axiom sets that have been proposed in the literature. This theoretical validation provides evidence that the measures really capture the internal attributes they purport to measure. This is a necessary precondition in the development of a set of measures for the internal attributes of concurrent software specifications