Formal Derivation of CSP Programs From Temporal Specifications

摘要: The algebra of relations has been very successful for reasoning about possibly non-deterministic programs, provided their behaviour can be fully characterized by just initial and final states. We use a slight generalization, called sequential algebra, to extend the scope relation-algebraic methods reactive systems, where between initiation termination is also important. To illustrate this approach, we integrate Communicating Sequential Processes linear temporal logic in show that associated calculus permits formal derivation CSP programs from specifications.