Modeling Dynamic Processes in TLA.
Georg Rock, Stephan Werner, Andreas Wolpers · 1999
The formal development method of VSE (Verification Support Environment) for state-based systems is based on a variant of TLA. VSE supports structured specifications, modular refinements, and also modular proofs. There are applications where one wants (or has) to consider an indefinite number of processes or even processes that are created and deleted dynamically. The general problem that arises in all these applications is that a process can no longer be identified with a (static) component of a VSE specification. Our main interest in this paper is in modeling dynamic processes in a uniform and generic way in VSE. 1