Project 2.1. Functions and predicates for the QL language to query time series data

Assignment 1 in CISC/CMPE 422 introduces a language called QL (for 'Query Language') to allow the formulation of queries over 2-dimensional arrays of integers. In the assigment, the arrays represent sales data (i.e., how many units of a specific product have been sold on a specific day). However, QL could easily be adapted to other time series data such as daily rainfall amounts or body temperature readings. A major drawback of QL is its lack of support for 'procedural abstraction'. I.e., it is currently impossible in QL to attach a name to an expression or formula and use that name to refer to the expression or formula. As a result, QL queries can become unnecessarily verbose, and hard to read, reuse, and modify.

Project 2.2. Implementation of an evaluator for predicate logic

The goal of the project is to implement an evaluator for a variant of predicate logic that allows bounded quantification over the natural numbers. To this end, the ANTLR parser generator is to be used.

The project is most suited for a student with interests language design and implementation (e.g., parser generation with ANTLR) in Java. Completion of CISC/CMPE 422 would be helpful, but not necessary.

Project 2.3. Constraint solving for the QL language to query time series data

Assignment 1 in CISC/CMPE 422 asks students to implement an evaluator for a query language called QL (for 'Query Language') for 2-dimensional arrays of integers. With the help of the evaluator, constraints expressed as QL formulas can be checked on specific 2d-arrays. Later in CISC/CMPE 422, constraint solving is introduced (in the context of Alloy). With constraint solving, instances satisfying given constraints can be generated. There currently is no way to generate 2d-arrays that are guaranteed to satisfy given QL formulas.

The goal of the project is to implement a constraint solver for QL. The solver should take a QL formula as input together with some kind of 'scope' constraint and produce an array satisfying the formula (if it exists) as output. The solver could be based on a 'brute-force' exploration of the, suitably bounded, search space, or use Microsoft's Z3 constraint solver.

The project is most suited for 1 or 2 students with interests in constraint solving and Java. Completion of CISC/CMPE 422 would be helpful, but not necessary.

Project 2.4. Exploring JavaMOP for runtime monitoring

Runtime monitoring is a software quality assurance technique in which relevant information is collected during runtime of the program/system and then checked for indications of failures or requirements violations. Monitoring typically requires instrumentation to cause the program to emit the relevant information in some form. Also, a monitor is required that checks the collected data. JavaMOP4 is an open-source tool that supports runtime monitoring of Java programs. It greatly facilitates the monitoring through the automatic instrumentation of the monitored program and the generation of a monitor from a high-level specification of the property to be enforced.

The goal of the project is to explore the use of JavaMOP. This will require installing the tool and trying it on a range of sample programs, some of which will be developed by the student.

The project is most suited for 1 or 2 students with interests in Java and software quality assurance.

Project 2.5. Autograding with GitHub actions

GitHub Actions allow the automation of software development activities and workflows such as building, testing, packaging, or deploying any code project on GitHub. In an academic context they offer the opportunity to support the automatic grading of assignments.

The goal of the project is to explore the use of GitHub actions to autograde assignments that involve the use of a formal specification and analysis tool such as Alloy or NuSMV.

The project is most suited for a student with interests in formal methods and GitHub. Completion of CISC/CMPE 422 would be an asset.

Project 2.6. Formalization and analysis of advanced data structures in Alloy

Alloy allows the expression and analysis of 'class models', i.e., formal specifications that capture constraints on objects and their relationships. These class models can be used to gain a deeper understanding of some domain and its properties, detect design flaws, or generate test cases.

The goal of the project is to use Alloy to formalize and analyze a suitable advanced data structure (such as Red-Black Trees).

The project is most suited for a student with interests in formal methods. Completion of CISC/CMPE 422 would be an asset.

Project 2.7. Exploring probabilistic model checking

Model checking is a software quality assurance technique based on the exhaustive exploration of the state space of the system with respect to temporal logic properties. Probabilistic model checking extends this technique to systems that exhibit uncertain or probabilistic behaviour. One of the most popular and mature probabilistic model checkers is PRISM. PRISM allows the automated analysis of a wide range of quantitative properties of these models such as "what is the probability of a failure causing the system to shut down within 4 hours?", "what is the worst-case probability of the protocol terminating in error, over all possible initial configurations?", or "what is the expected size of the message queue after 30 minutes?".

The goal of the project is to explore the use of PRISM for the specification and analysis of probabilistic systems. This will require installing the tool and trying it on a range of sample systems, some of which will be developed by the student.

The project is most suited for a student with interests in formal methods. Completion of CISC/CMPE 422 would be helpful, but not necessary.

Project 2.8. Formalizing Git

Git is one of the most popular and powerful version control systems. However, it is also quite complex containing a rather large number of concepts (e.g., repositories, directories, files, branches, heads, tags, submodules) and operations (e.g., init, clone, add, diff, commit, fetch, pull, push, retore, reset, branch), making it challenging to learn.

The goal of the project is to perform a 'domain analysis' of Git and construct class models that capture the most important concepts in Git and their relationships. Moreover, the effect of operations could be captured through constraints in the form of pre- and post-conditions. The use of Alloy is recommended, but not required.

The project is most suited for a student with interests in formal methods. Completion of CISC/CMPE 422 would be helpful, but not necessary.