A framework for multi-notation requirements specification and analysis

Many organizations desire the convenience of using multiple notations within a requirements specification. Rather than using separate tools for each notation, we advocate combining the parts semantically for tool-based analysis. We describe a framework for integrating notations from four distinct categories, namely “models”, “events”, “actions, and “expressions”. The categories allow us to view the notations independently but in a manner whereby they can be combined to create a specification. The categories are implemented as types in higher-order logic. Typechecking ensures conformance to the rules for combining notations. Our choice of higher-order logic as a base formalism allows the framework to support notations with uninterpreted constants. With our framework, it is possible to use new combinations of notations without changing existing notations or rebuilding formal analysis tools such as model checkers