This paper discusses experiments with a "model-based" approach for developing verified distributed systems in which program development is carried out by stepwise refinement: we encode, specifications and algorithm archetypes in the PVS theorem prover, carry out stepwise refinement and concomitant proofs, and obtain collections of verified algorithms encoded in PVS. Finally we transform algorithms from PVS to programs in Java. We consider a class of systems in which state spaces may be continuous and state transitions may be continuous or discrete. Coordinated multi-vehicle systems are examples of this class. Temporal properties of this class of problems are specified in terms of convergence: the system state gets arbitrarily close to a limit as time tends to infinity. Our meta-theorems for verifying convergence are extensions from control theory to a temporal logic of continuous time and state spaces.

Attachment | Size |
---|---|

vstte.pdf | 319.75 KB |

cgmw-refinement.pdf | 390.29 KB |