ISBN : 978-81-963532-2-3 (E-Book) different specification languages. Some of these specifications describe the system’s behavior and the others describe the system’s structure. Consequently, two broad classes of semantic abstraction functions are defined: those that preserve a system’s behavior and those that preserve a system’s structure. Model-oriented vs. property-oriented approaches Formal methods are usually classified into two broad categories – model – oriented and property – oriented approaches. In a model-oriented style, one defines a system’s behavior directly by constructing a model of the system in terms of mathematical structures such as tuples, relations, functions, sets, sequences, etc. In the property-oriented style, the system's behavior is defined indirectly by stating its properties, usually in the form of a set of axioms that the system must satisfy. Example:Let us consider a simple producer/consumer example. In a property-oriented style, it is probably started by listing the properties of the system like: the consumer can start consuming only after the producer has produced an item; the producer starts to produce an item only after the consumer has consumed the last item, etc. A good example of a producer-consumer problem is CPU-Printer coordination. After processing of data, CPU outputs characters to the buffer for printing. Printer, on the other hand, reads characters from the buffer and prints them. The CPU is constrained by the capacity of the buffer, whereas the printer is constrained by an empty buffer. Examples of property-oriented specification styles are axiomatic specification and algebraic specification. In a model-oriented approach, we start by defining the basic operations, p (produce) and c (consume). Then we can state that S1 + p → S, S + c → S1. Thus the modeloriented approaches essentially specify a program by writing another, presumably simpler program. Examples of popular model-oriented specification techniques are Z, CSP, CCS, etc. Model-oriented approaches are more suited to use in later phases of life cycle because 30 Software Engineering Keerthana P, Manasa KN, Ganga D Bengal
36 Publizr Home