Formal approach to specification and verification of task management in interactive systems

An approach to the formal specification of task management models for interactive systems is presented. The approach is well suited to data-intensive applications where the system is being used to manage complex collections of interrelated objects. The approach consists of annotating objects with status information, and relating status back to properties of the underlying collection. Status information is used to guide and control the application of activities. The approach is illustrated with an example from interactive theorem proving