Semantic Validation of Product and Process Models

Abstract

This paper describes the use of equational specifications and process algebras in developing product and process models. These formal approaches enable an abstract and precise description of products, where both syntactic and semantic checks are used for validation. In addition, refinement methodologies are provided that relate the abstract specifications to implementations in data modeling languages such as EXPRESS. We show how these formal approaches, initially designed for specifying software and hardware modules, relate to current standards and research in product and process modeling. Our approach is illustrated with examples of both product and process modeling. The general architecture engineering and construction reference model (GARM) is modeled in an equational style using the Larch family of specification languages. The partitioned engineering data flow model (PANDA), a graphical approach for describing process models in facility engineering, is modeled as a process algebraic system in calculus of communicating systems (CCS). Both examples are validated by proving that they satisfy certain syntactic and semantic properties.