Abstract: |
The Trace Function Method (TFM) is a fundamental approach to the description of system behavior for requirements analysis, specification, and documentation. External behavior of systems or components is given in mathematically direct form, but with full abstraction from internal state, by defining output at discrete interface events as recursive functions of the complete history of previous interaction at the same interface, including both input and output. In order to understand and evaluate the semantics of the notation, and in particular the executable semantics, that is, the potential for automatic simulation and construction of prototype implementations
from TFM descriptions, a recursion-theoretic analysis is given. It is demonstrated that a single run and the full reactive behavior of a TFM description can be presented as instances of first-order and higher-order course-of-value iteration, respectively. A simple sufficient condition for correct implementations of TFM descriptions in terms of state systems is given. The spectrum of possible state-based implementations of a TFM description, ranging from straightforward simulation to minimized state space, is explored. Implications for semantically calculated and hence formally verifiable prototype implementations are summarized. |