{'fraction_non_alphanumeric': 0.03114754098360656, 'fraction_numerical': 0.008743169398907104, 'mean_word_length': 5.4020979020979025, '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 Semantics-Based Approach for Mapping Specification Notations to Analysis Tools

Model-based notations (e.g. statecharts [7, 8], RSML [14], CSP [10], CCS [17] and LOTOS [11]) have been widely used by practitioners to describe software systems. They have intuitive step semantics and their composition operators provide facilities for decomposing large problems into modules and for expressing concurrency, synchronization and communications among modules. Many well-established analysis tools, such as model checkers, have been successfully applied to verify automatically model-based specifications. In order to analyze specifications in a model-based notation, either an analyzer is constructed specifically for the notation or a translator is written from the notation to the input language of an existing analysis tool. Translation is a common approach for reusing existing tools to analyze a specification without rewriting it by hand [1, 2]. However, a translator needs to be constructed for each notation and needs to be changed whenever the syntax or the semantics of the notation evolves. To help tackle these problems, we and other researchers propose approaches to generate analyzers automatically from a description of a notation’s semantics [4, 6, 20]. In these approaches, the semantics of a notation are defined and fed into an automatic analyzer generator and a compiler for that notation is produced. The compiler takes a specification in that notation as an input, and it automatically generates a transition-relation for the specification. Transition-relations form the basis of most analyzers, so a transition-relation representation of the specification can be checked using many automatic analysis tools, such as model checkers. Problem Statement: Because the semantics of model-based notations are complex,