{'fraction_non_alphanumeric': 0.011385199240986717, 'fraction_numerical': 0.0, 'mean_word_length': 5.1796875, '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}}
Proving specifications of tasking systems using Ada/TL

ADA/TL is a language for specification of the behavior of systems of communicating tasks. It merges concepts of the specification part of ADA, VDM specification of packages, and temporal logic specification of task behavior. The TL part consists of constructive specification of behaviors of individual tasks and a system specification of the properties of the interaction of tasks. A proof of a system specification consists of showing that the system property holds over all possible interleavings of the task behaviors.
This paper extends earlier work on proof of system specifications to cover more general branching behaviors of individual tasks, including cases of timed task calls and timed rendezvous. The constructive specification of each individual task defines a finite state computation model of its possible behaviors with allowed communication between task computations. The proof system uses marker symbols to represent the current state within each task computation, inference rules to justify transformations from one state to the next, and a proof tableau for representing the proof steps. The method rests upon the technique of using an invariant system property to identify a finite computation model of the interaction of all the system tasks. The proof tableau symbolically traces threads of control in all branches of the finite state model of the interaction of all of the system tasks. The proof method is illustrated herein using an example of a traffic walk-light controller with a timed behavior.