Chapter 6
Execution
The future will be better tomorrow.
—Dan Quayle
In this Chapter, we will:
- [INTRODUCTION] look at several ways of generating a program from a PTL specification (Section 6.1);
- [TECHNIQUE] describe the METATEM approach to the direct execution of PTL specifications (Section 6.2);
- [SYSTEM] examine the Concurrent MetateM system which implements the METATEM approach, bringing in deliberation, concurrency and multi-agent systems (Section 6.3); and
- [ADVANCED] highlight a selection of more advanced work including both extensions of METATEM and alternative approaches to implementing temporal specifications (Section 6.4).
Relatively few exercises will appear in this chapter, but the solutions to those that do can, as usual, be found in Appendix B.
6.1 From Specifications to Programs
We have already seen, earlier in this book, how temporal formulae can be used to describe individual computational components. In addition, we have seen that temporal formulae can usefully describe properties of existing programs (and that these properties can sometimes be checked via model-checking techniques). However, there is a gap here between the specification of a component and its actual implementation.
As in many formal methods, there are several ways to move from a formal specification of a component to an implementation of that component (that satisfies the specification). The most common techniques for achieving this are refinement, synthesis and direct execution.
6.1.1 Refinement ...
