Model-based software design and validation

摘要: A new computer language, which is based on a formal, mathematical state-machine model, and used both to validate generate code for distributed system, in general, enables developing system using multiple related specifications, instance, specifications at levels of abstraction or decompositions into parallel combinations interacting systems, allows use validation tools verify properties these systems their relationships. The language includes constructs specifying non-deterministic actions, constraints those choices. Several well-defined sub-languages the full are also defined. These specify input some tools, particular, generators. One method software implementation present invention accepting design specification applying procedure that has desired properties. This theorem proving specification. generating implementations components system.