Qubie, also known as the Poll Queue Monitor, is a part of the Free & Fair suite of products. It is a compact polling place monitoring system that attempts to estimate the wait time for casting a vote. It can be used by jurisdictions to gather data about polling place usage and performance, for use in allocating resources for future elections. It can also optionally make wait time information available on the Web in real time, so that voters can accurately gauge how long the voting process will take them and plan accordingly (by choosing among polling places, if they have multiple options; by voting at a different time; or, in jurisdictions with early voting, by voting on a different day). The system has two main components: a small open-source hardware box running open-source software that monitors a polling place for mobile device activity, and an optional application that makes wait time estimates available online.
Correctness of the software components of the system, and privacy and security guarantees with respect to the individually identifiable data they detect, are critical aspects of this project.
Prototype implementations of Qubie were developed as a part of the DemTech Research Project at the IT University of Copenhagen in 2011-2015 and were tested at Danish polling places. This implementation of Qubie is being developed completely from scratch, independently of the original project.
Qubie is being developed using the Trust-by-Design (TBD) software engineering methodology. The initial prototype version, available in the "prototype" directory, uses a subset of this methodology.
The TBD methodology is documented in several papers published by Joe Kiniry and his coauthors, available via http://www.kindsoftware.com/. In particular, read "Secret Ninja Formal Methods" and "A Verification-centric Software Development Process for Java", both of which were written with Dan Zimmerman.
In general, a system is comprised of:
a top-level readme (like this one) that includes information about the system's purpose, examples of its use, fundamental concepts, system requirements, and background literature,
a domain analysis and a detailed architecture specifications written in the Extended Business Object Notation (EBON),
where applicable, formal specifications written at the source code level in one or more contract-based specification languages like Code Contracts (for .NET systems), the Java Modeling Language (for JVM systems), or the Executable ANSI/ISO C Specification Language (E-ACSL),
protocol descriptions typically formally specified using abstract state machines (ASMs), petri nets, formally annotated collaboration diagrams, or other formal notations that have tool support for reasoning about such protocols,
a hand-written set of (sub)system tests and an automatically generated set of unit tests (using, e.g., PEX for .NET systems and JMLUnitNG for JVM ones), including reports on the completeness and quality of these validation artifacts, and
a set of evidence that the system fulfills its requirements, usually in the form of traceable artifacts from the requirements to other artifacts that validate that they are satisfied (e.g., test results, code reviews, formal proofs, etc.).
What follows are the mandatory and secondary requirements imposed upon Qubie. Informal verification (in the traditional software engineering sense) of these requirements is accomplished by several means, including formal verification of properties of the system's specification and implementation, as well as traceability from the requirements to artifacts that validate that they are satisfied (e.g., system tests, code review, etc.).
Development on the prototype version of Qubie is taking place on the Raspberry Pi platform. It is dependent on the following libraries, tools, and frameworks:
The source code is currently under development for use on an embedded system with a minimal OS (e.g. rtos) and depends onf the following libraries, tools, and frameworks: