Michael Jones, PhD

Its mostly about a framework for comparing and contrasting different formalisms. But, there's a set of three trace algebras for embedded software. Of those three, the "Metric time" model is most similar and interesting relative to our timed semantics for machine code.

The metric model:

• has a continuous model of time in which time is modeled on the reals.
  
• allows real and integer valued variables.
  
• A partial trace is a sequence of triples gamma, delta and f. delta is the duration. gamma is the signature and f is a function, with domain [0,delta], that: gives values as a function of time, and maps input or output events to times.
  
• the mapping of a variable to a value wrt time must be piece-wise continuous and right-hand limits must exist at all points.
  
• f(a)(t) == 1 means that event a occured at time t.
  

A complete trace is a pair, gamma and f, where gamma is the signature and f is a function. The function f is defined as before except f is defined over the non-negative real numbers rather than the range [0,delta] .

Then you can do projection, renaming and concatentation.

So, relative to our model, our model is discrete time and discrete valued on the inside but allows time varying functions of real time over real values in the environment. Our model starts with a specification language (I suppose that's what we'd call it) then gives the interpretation of a system. That's a little different because their algebra gives a formalism for manipluating traces that might result from a system such as ours. So, we can specify signatures then their formalism could represent the behaviors of our system and be used to do projection, renaming and concatenation.

Seems that their formalism is more powerful than ours. They have real time and real valued variables. We don't. I think we could express all of our models in their trace algebra. We can't write models that generate all ofthe traces they can model.

Open questions: what verification algorithms and properties can be defined on the traces?

In Smolka's classification scheme this would be an interleaved extensional model and ours is an interleaving intensional model. Smolka claims, and I agree (for what its worth) that "Extensional models provide a useful basis for explaining system behavior, while intensional one are more amenable to automated analysis." And so it would make sense that we are going extensional.