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 software 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. The 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 sets of properties that have been proposed in the literature. This theoretical validation provides supporting 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