Dynamic Environment Generations for an ASTRAL Process

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.