{'fraction_non_alphanumeric': 0.0223431124927142, 'fraction_numerical': 0.0, 'mean_word_length': 5.209891435464415, '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}}
Temporal assertions for sequential and concurrent programs

In this thesis, we present an extension to the well-known concept of assertions: temporal assertions allow the specification and validation of modal safety properties of an application at runtime. We see this as a necessary step in enforcing the growing number of implicit requirements of software specifications, which are often only informally defined in the documentation of application program interfaces (API) and are beyond the reach of type checkers, compilers, or model checkers. Also, we show how our techniques can be applied to existing programs without modifying the source code. Although, like assertions, our approach cannot prove the absence of errors, it gives the programmer a more powerful means of automatically checking assumptions about his program at runtime. It can also be used to look for behaviour that indicates the potential for problems, that is, that might be used to predict future errors. An example is the Lock-order Reversal pattern which indicates a potential deadlock in a concurrent program. Our parametrised propositions approach gives us a convenient way to handle dynamic systems: in real-world programs, almost always dynamic data is used, for example, new objects are instantiated, or new threads created. While there is already a plethora of work on checking some properties of those systems, they are usually concerned with the boundedness of the number of resources, and not necessarily with the interaction of those objects. Especially, they are often limited to either non-recursive examples or some coarse finite abstraction. Propositions in our practical examples are certain events which we can observe in the execution of a program: method invocation with caller/callee and arguments, object attribute access, or actions related to concurrency. If we have a property which has to be checked on a per-object basis (that is, instantiated for each object or set of objects), our template mechanism dynamically instantiates a given formula based on observers, so-called existence predicates. In a static approach, this would have to be solved by generating all instances of the property beforehand and checking each of them against the model, leading again to a finitary abstraction. As application, we see two kinds of properties: firstly, properties over the universal behaviour of data structures. For example, it universally holds that a pop from a stack should not be performed unless something has actually been pushed onto it. Data structures and their respective functionality are usually accumulated in libraries. Thus, a test facility implemented in the library should be available to any application using it. Furthermore, the corresponding formula can be used very much like a design pattern from Software Engineering and new implementations of some previously specified behaviour can be checked against the temporal specification of the pattern. Secondly, there are application specific properties. These can be based, for example, on the specification that defined the application. Or they can be derived from informal requirements, stated in the documentation. Rather than being invariants of a structure like above, they may not be evident and need to be “developed” as much as the source code for the application has to be developed. As a lot of current research also focuses on documenting and enforcing such specifications, we later comment on the necessity and advantages of storing such semantic annotations about the application in a machine-readable format. Naturally, the additional level of possible checks comes at a penalty: runtime overhead. In the most general case, for every event, the set of affected state machines (the automaton-based representation of the property) must be determined. This also includes possibly instantiating new ones. Then, in each machine, a state transition must be triggered. As the underlying framework of our mechanism is based on alternating finite automata, we already incur an exponential blow-up in the size of the automaton when moving to nondeterministic automata. The additional determinisation of said nondeterministic automata will make this approach infeasible in practice. Instead, we will resolve the nondeterminism at runtime at the cost of performance: after statically generating an alternating finite automaton from the formula and eventually pre-calculating the (nondeterministic) outgoing edges for each state, we use a breadth-first approach over the branches for checking the acceptance condition of the input. We will see that this solution has double-exponential overhead, but we still consider it as a useful tool, since the average behaviour might prove not to be as harsh as this complexity might suggest. Also, using our algorithm offline, on a recorded trace, is an option that does not slow down the actual application. Practical examples from object-based and concurrent programs written inHaskell, C, and Java underline the general usefulness of the approach. A proof-of-concept prototype developed in Java confirmed the practicality of our approach.