Development of Reactive Systems: Property-Based vs. Model-Based

                            Amir Pnueli

        New York University and Weizmann Institute of Science


There are two major styles for the specification of reactive systems,
which have a major impact on the way such systems are rigorously
developed and verified. The property-based approach presents a
specification as a collection of requirements, each identifying a
desired property that the system should satisfy. A great advantage of
this approach is that it makes the specification highly modular: it is
very easy to add or remove a requirement. On the other hand, altering
a single property may have impact on all components of the
implementation. Typically, a property-based approach may use a logical
language such as temporal logic for the specification of individual
properties.

A different approach is presented by the Model-based style, in which a
system is specified by an abstract program (a model) which captures
the expected functionality of the system. In this approach there is a
much closer correspondence between the structure of the specification
and that of the implementation. Namely, minor changes in the
specification result in small changes in the specification.

Another characterization of these different approaches is that the
model-based approach projects all the behavioral elements on each
object (component) separately, while the property-based approach
assembles these elements along different scenarios.

In the talk, we will discuss and compare these different approaches
and explore the impact these styles have on the development and
verification of reactive systems, assessing their relative merits for
the construction of a verifying compiler based on these approaches.