Formal techniques for systems specification and verification

摘要

An information system is an agent that keeps its own database, may communicate with other systems through messages and performs some activities. A layered approach is proposed for information systems specification and verification, according to the Infolog model. This formal approach includes five layers: the first two layers are concerned with the specification of safety constraints on the envisaged system database (both static and transition constraints); in the third layer we describe the application-dependent operations by their properties; in the fourth layer we specify a set of liveness and other requirements on the system evolution and we describe its communication behavior; and in the last layer we specify the activities that the system should perform in reaction to trigger events. Each layer should comply with the specification of the previous layer. A unifying, logical framework is proposed supporting the layered approach. The framework includes linear logics for some layers and branching logics for other layers, depending on the type of requirements and constraints relevant in each layer. Both proof-theoretic and model-theoretic techniques are used when introducing the unifying approach.