Abstract
Dynamic Environment Generations for an ASTRAL Process
by: Z. Dang and R.A. Kemmerer
Abstract:
ASTRAL is a high-level formal specification language for real-time systems. Itincludes structuring mechanisms that allow one to build modularizedspecifications of complex real-time systems with layering. Based upon theASTRAL symbolic model checker reported in [DK99b], an approximation techniqueto speed-up the ASTRAL symbolic model checker for debugging a specification ispresented. The technique, called dynamic environment generation, randomlygenerates a sequence of concrete environments for an ASTRAL process instancealong each execution path in the execution tree of the ASTRAL process. Doingthis greatly reduces the time for finding an error in a specification, asdemonstrated by a number of mutation tests, while still ensuring reasonablecoverage of the search procedure. The results of the tests show that thetechniques presented in the paper are effective.
Keywords:
ASTRAL, formal methods, formal specification and verification,model checking, real-time systems, state machines, timingrequirements
Date:
March 2000
Document: 2000-03
