Tools for Simplifying Proofs of Properties of Timed Automata: The TAME Template, Theories, and Strategies.

reportActive / Technical Report | Accession Number: ADA361638 | Open PDF

Abstract:

The tool TAME is intended to provide automated support to simplify specifying and reasoning about timed automata using PVS. This report documents the current specification template, standard theories, and PVS strategies upon which TAME is based. The TAME system is now available for limited distribution by contracting the author.

Author(s):
Archer, Myla
Author Organization(s):
NAVAL RESEARCH LAB WASHINGTON DC
Supplementary Note:
DOI: 10.21236/ADA361638
Pagination:
0056

Security Markings

DOCUMENT & CONTEXTUAL SUMMARY

Distribution:
Approved For Public Release

RECORD

Collection: TR
Identifying Numbers
Report Number(s):
NRL/MR/5540--99-8359
Monitor Series:
ONR
 Subject Terms
Joint Capability Areas:
JCA_5_Command and Control; JCA_5.3_Planning; JCA_1.2.5_Lessons Learned; JCA_5.2.2_Develop Knowledge and Situational Awareness; JCA_5.2_Understand; JCA_8_Building Partnerships
Modernization Areas:
AI and Machine Learning
Communities of Interest:
Sensors
Descriptor(s):
*AUTOMATION, *VERIFICATION, *AUTOMATA, SPECIFICATIONS, TOOLS, REASONING, THEORY, TIME, TEMPLATES
Field(s)/Group(s):
Cybernetics
Keyword(s):
PE62234N
Report Date:
1999 Mar 26
Creation Date:
1999 Apr 21