{'fraction_non_alphanumeric': 0.01978891820580475, 'fraction_numerical': 0.0, 'mean_word_length': 5.268595041322314, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Simulation Based Model Checker for Real Time Java

The Real Time Specification for Java (RTSJ) is an augmentation of Java for real time applications. The possibility of applying a model checker to RTSJ has great appeal given the complexity and safety requirements of its intended applications. The Robust Software Systems group at NASA Ames Research Center has Java PathFinder (JPF) under development, a Java model checker. JPF at its core is a state exploring JVM which can examine alternative paths in a Java program (e.g., via backtracking) by trying all nondeterministic choices, including thread scheduling order. This paper describes our implementation of an RTSJ profile (subset) in JPF, including requirements, design decisions, and potential future extensions. The implementation relies on a discrete event simulation library, which enables modeling and verification of an RTSJ application under a programmed test environment. The primary advantage of this approach is the possibility of direct execution of the combined model on ordinary Java systems (without the benefit of state backtracking or cost accounting); the primary drawback is the difficulty of implementing important RTSJ features such as non-heap memory areas and asynchronous control transfers. The utility of a general model checker such as JPF in finding RTSJ logic and timing errors is discussed, as well as opportunities presented by JPF for more advanced forms of program analysis such as symbolic execution and test input generation.