We describe a framework where formal models can be rigorously defined and compared, and their interconnections can be unambiguously specified. We use trace algebra and trace structure algebra to provide the underlying mathematical machinery. We believe that this framework will be essential to provide the foundations of an intermediate format that will provide the Metropolis infrastructure with a formal mechanism for interoperability among tools and specification methods.
Jerry R. Burch, Roberto Passerone, Alberto L. Sang