Theorem Proving in Higher Order Logics

DOVE is a Isabelle-based, graphical tool for the trusted design and analysis of state machine designs. Work is currently underway aimed at increasing the scope of DOVE to include complex, dynamic and real-time processes. This paper describes a refinement approach to the design and analysis of complex processes, including a formal development of the approach in Isabelle. It is argued that the addition of a network feedback operator and associated refinement rules makes the refinement calculus of Back a powerful development tool for process networks, allowing essentially arbitrary decomposition of network properties over subcomponents. The feedback operator is shown to be ‘compositional’ with respect to an implementation language of digital input/output processes with local state. Some simple examples are considered.