CISC835: Formal Methods in Software Engineering (Fall 2019)
Projects
Choosing a project
The projects for CISC835 can be worked on in groups of 1 or 2 students.
In general, different kinds of projects are possible, including:
Apply the course material to a new problem; e.g.,
use one or more of the languages and tools
presented in the course to formalize and analyze one
or more problems or puzzles (e.g., the RushHour
puzzle www.puzzles.com/products/rushhour/rhfrommarkriedel/Jam.html).
You might even be able to
find a suitable problem in your area of research.
Explore work that extends the material discussed in class; e.g.,
you could investigate and experiment with any of the tools mentioned below
in the list of tools
or compare some of them with tools discussed in class or other tools on the list.
Proposal
The proposal should describe the problem to be solved or work to be carried out,
material or software to be used, together with any challenges and results expected.
The length should not exceed 2 pages.
The proposal is due Wednesday, November 10 in class.
Please use the ACM SIG Proceedings format when preparing your
proposal. Templates for Word, Word Perfect, Latex
are available
here.
The proposal is due on Monday, Oct 28.
Presentation
Project presentations will be held during the week of December 2, 2019.
Please note:
Each presentation has a 25 mins slot. Of these 25 mins, 20 mins should
be used for the presentation itself, while the remaining 5 mins are
for questions and discussion. Please ensure that your presentation
does not take longer than 20 mins. If you do take longer, I will have
to interrupt you.
The 5 mins discussion period will also be used to
allow the next speaker to get ready.
Please make sure prior to your
presentation that your laptop works with the data projector in the
class room.
The content of each presentation should
be understandable to the majority of the members in the class,
explain any background or context information or material necessary to understand or appreciate what you have done,
summarize what you have done and why it is interesting and worth doing,
briefly describe how you have done it,
mention which results you have obtained and what you have learned (e.g., what would you do differently next time?),
share any additional observations that you feel are relevant or interesting.
The presentation slides should
be correct, clear, readable and easy to navigate; typically, that means that slides should not contain a lot of text; highlighting of text can be very useful to emphasize key points; diagrams can be very useful to communicate concepts and relationships effectively, and
support and be connected to what you say.
The delivery of the presentation should be clear, engaging and
easy-to-follow, i.e., try to speak clearly with appropriate
pace (i.e., neither too fast, nor too slow) and good eye contact.
Final report
The report should describe the problem or issue that your project addresses
and why it is important. It should describe the work that you have done,
and any ideas
or insights it is based on. Relevant observations and lessons learnt
about the project or any part of it should be included. Finally, the work
should be placed into the context of the course and any related work should
be sketched briefly.
The length should not exceed 10 pages.
Please use the ACM SIG Proceedings format when preparing your
proposal. Templates for Word, Word Perfect, Latex
are available
here.
Evaluation
The project is worth 20% of your overall mark in the course with the following
breakdown:
Presentation: 7%
Proposal and final report: 6%
Evaluation (i.e., overall difficulity and quality of work carried out): 7%
Project presentation schedule
Presentations will take place on Thursday, Dec 5, from 1:30pm to 4pm, in Goodwin 536. Presentations will proceed in this order. Times are approximate.
1:30-2pm, "Exploration of different versions of Alloy" (Sahil)
2-2:30pm, "Using Alloy Analyzer to Model a Solution to the Assignments Problem Through the Context of Post-Secondary Roommate Matching" (Robyn)
2:30-3pm, "Survey of Formal Verification Techniques for Deep Neural Networks" (Rebecca)
3-3:30pm, "Monitoring Events using the BeepBeep 3 Event Stream Processor" (Isra and Mufasir)
3:30-4pm, "Higher-Order Model Checking, Program Verification, and Refinement Typing" (Dimitrios)
Tools list
Propositional and predicate logic
A list of theorem proving tools can be found
here.
Constraint solving generalizes checking for satisfiability or validity
discussed in class; constraint solving is discussed in more
detail here.
Popular constraint solvers include:
Z3 from Microsoft and
Choco.
Class modeling
A list of applications of Alloy can be found here.
DynAlloy
is an extension of Alloy that allows the description of dynamic (i.e., behavioural) properties
using actions.
Alloy* is an extension of Alloy that expands the set of specification that can be analyzed (by supporting quantification over higher-order structures such as relations)
A list of other tools built on Alloy (or its underlying model finding technology) can
be found here.
The Object Constraint Language (OCL) is a more mainstream technique to express
object constraints. You can find a description of OCL
here.
Popular OCL tools include
USE and
and Dresden OCL.
A more complete list of OCL tools is
here.
The Java
Modeling Language (JML) allows the embedding of formal specifications
and constraints right in Java. Supporting tools are listed on the JML pages.
Model checking
Apart from NuSMV,
Spin
is one of the most well-known model checkers.
Java Pathfinder
is a software model checker, i.e., it can explore the state spaces
of Java programs directly and without prior translation to some
tool-specific input language.
For finite state machines with time (a.k.a., Timed Automata),
the UppAal is most widely used
For finite state machines with probabilities on the transitions (a.k.a, Markov Chains),
the PRISM model checker is the state-of-the-art.
Other verification and analysis tools
The Rise 4 Fun site contains
lots of tools for different kinds of analyses.
Formal methods for deep learning
Neural nets have proven very useful. However, to be able to use them in
safety critical applications, we need to be able to validate, verify, and even
certify them. Research on this topic is still in its infancy. The project
could survey some of the ideas that have been proposed.
Machine learning for formal methods
Could machine learning be leveraged for the formal analysis of software
artifacts? Could, e.g., learning techniques be used to learn formal
specifications, find useful abstractions for complex systems, or
fine tune and optimize the use of an analysis tool?
The project could survey some of the ideas that have been proposed.