System Architecture Specification Based on Behavior Models

摘要

This paper suggests an approach to formal software and system architecture specification based on behavior models. The behavior of the system is defined as a set of events (event trace) with two basic relations: precedence and inclusion. The structure of event trace is specified using event grammars and other constraints organized into schemas. The framework provides high level abstractions for analyzing system behavior properties expressed as computations over event traces. The automated tools can support extracting of different views from the model, and verification of behavior properties within a given scope. Advantages of this approach compared with the common simulation tools are as follows. Means to write assertions about the system behavior and tools to verify those assertions. Exhaustive search through all possible scenarios (up to the scope limit). The small scope hypothesis states that most of errors can be demonstrated on small examples. The support for verifiable refinement of the architecture model, up to design and implementation models. Integration of the architecture models with environment models for defining typical scenarios (use cases) and verifying system's behavior for those scenarios.