In this paper, we propose a compositional approach to constructing correct formal models of information systems from correct models of interacting components. Component behavior is represented using workflow nets - a class of Petri nets. Interactions among components are encoded in an additional interface net. The proposed approach is used to model and compose synchronously and asynchronously interacting workflow nets. Using Petri net morphisms and their properties, we prove that the composition of interacting workflow nets preserves the correctness of components and of an interface.
翻译:在本文中,我们提出一种组成方法,用正确的互动组件模型来构建正确的信息系统正式模型。组成部分行为用工作流程网(一种Petri 网类)来代表。各组成部分之间的相互作用在另一个接口网中编码。拟议办法用于模拟和形成同步和不同步互动工作流程网。我们利用彼得里网络形态及其特性,证明互动工作流程网的构成保持了各组成部分和接口的正确性。