State-Machine Modelling in the DOVE System

Abstract

The DOVE tool supports high-level system modelling and design, and formal reasoning about critical properties. DOVE uses state-machine graphs to illustrate designs, thus building on a familiar and effective means of communicating system designs to a wide audience. DOVE employs a propositional temporal logic to express desirable behavioural properties of the design, and presents it in a sequent calculus syntax for ease of manipulation. A verification procedure which can handle temporal properties of DOVE state machines is included through high level tactics in a graphical proof tool interface. The DOVE program is committed to developing proof visualization techniques to complement the power of this proof scheme. This paper presents the theoretical structure underlying the DOVE tool.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 01, 2003
Accession Number
ADA417282

Entities

People

  • A. Can
  • B. Mahoney
  • C. Liu
  • J. Mccarthy
  • K. Eastaughffe

Organizations

  • Defence Science and Technology Group

Tags

Communities of Interest

  • C4I
  • Cyber

DTIC Thesaurus Topics

  • Abstracts
  • Australia
  • Computations
  • Computer Network Security
  • Computer Programming
  • Computer Science
  • Computers
  • Concrete
  • Construction
  • Engineering
  • Information Science
  • Language
  • Security
  • Standards
  • Topology
  • Universities
  • Visualizations

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.
  • Systems Analysis and Design