|
Description:
|
This project investigates formal uses of diagrammatic information in
verification. Designers use diagrams (such as timing diagrams,
circuit diagrams, and state machines, among others) heavily in their
work. Although many verification tools provide diagrammatic
interfaces, few of them treat diagrams as formal objects in their own
right. This project considers diagrams as logical systems,
investigating whether any of the properties that make diagrams
appealing to designers offer theoretical advantages to verification.
At present, we are implementing a verification tool based on a formal
logic of the interactions between diagrammatic and sentential
information. We are also working on decidability results and
algorithms for language-containment based verification with timing
diagrams as a specification language.
|