Cheap air quality monitoring

January 16, 2017

About a year ago I set up an air quality monitoring station based on the Air Quality Egg product by Wicked Device (see also my previous post on AQE). It was working during the winter season, providing real time data on PM2.5 concentrations near my house. This graph shows some of the data collected.

This worked OK, except that the data from the device was uploaded to Xively and available only from there. Xively was providing this service free as it was fulfilling an old commitment from one of their acquisitions. It was not high on their priority list and the service was frequently down. I decided to build my own device then to have full control over the process – from collecting the data to displaying them on a public web page. And to have some creative fun. The result works well (at least at the time of the writing) and cost less than $80 in materials, including a Raspberry Pi that I used. I think building a PM2.5 monitoring station in a way similar to what I describe below would make an excellent high school project.

Hardware

Initially I was planning to use the Shinyei PPD 42NJ particle sensor as the heart of the device. This is what was used in the Air Quality Egg that I got (they use a different sensor now). The performance of Shinyei PPD 32NJ has been independently evaluated. However, this part has to be individually calibrated, which I tried to do by taking it to Wrocław (I work there) and comparing the readings from it to the official monitoring station. The PM2.5 values in the city at that time were oscillating between 20 and 45 µg/m³, which was not wide enough range to get a good correlation. Or maybe it simply didn’t work for some other reason. After a month of unsuccessful attempts, I decided to buy SDS011 sensor made by Nova Fitness Co., Ltd. It is more expensive ($25 on AliExpress rather than $10), but provides actual PM2.5 and PM10 readings in µg/m³ through its serial interface. The two units I ordered came with TTL to USB adapters. One of the adapters didn’t work, but I could easily replace it with another one I bought locally for about 2$. So, hardware-wise all one needs to do is to put the SDS011 sensor in a box with some holes and connect the USB side of the adapter  (through some extension cable) to a standard USB port. Here is how it looks like in my case:

20170115_202804

I would like to make it clear here that I am showing this picture not to demonstrate an example masterpiece of industrial design, but as evidence that if I can do it, everybody can.

The other end of that USB cable connects to a Raspberry Pi with software described below. I chose Raspberry Pi for ease of programming, but I guess Arduino is an option as well. The adapter shows up as /dev/ttyUSB0 device on Linux and transmits a 10-byte message once a second.

Software

The software stack that runs on a Raspberry Pi consists of five KDB+ processes managed by Enterprise Components middleware. All relevant code and EC configuration is on GitHub. Out of that code probably the sds.c file might be interesting as it contains the TTY interface configuration that took me some time to figure out. That file does not contain any KDB+ related stuff, so it can be compiled into a library for getting data from SDS011 on Linux. There are a couple of other projects related to SDS011 on GitHub, so if you do your own setup don’t forget to do a search to find the most useful one.

Using an industrial strength time series database for collecting 1Hz data may seem like an overkill and that’s because it is. But, since KX released a Raspberry Pi build of their product I wanted to try it out with Enterprise Components to which I contributed some code. Everything worked pretty much out of the box. The only thing that I spent some more time on was building yak (the process manager for the Components). yak is written in Python and it is usually used in executable form made by bbfreeze. The instructions for building yak that can be found on its GitHub repository worked on Raspberry Pi, except that I had to install patchelf-wrapper as an additional dependency. All that KDB+/EC stack can be easily replaced by a simple Python script logging the data in CSV files and uploading the current values to the some publicly available place.

In my case the current data in JSON format are rsync’ed to the hosting service every 10 minutes. I used this guide to setup rsync so that providing password with every connection is not necessary. The result can currently be viewed here. The html file there is a simple web app written in Elm, but that’s just because I wanted to keep somewhat current with changes in Elm (they dropped signals – one of their core concepts with their 0.17 release in May last year). The same thing can be done by generating a static page every 10 minutes, or whatever frequency one wants to update the value with.

 

IsarMathLib 1.9.4 and other news

April 17, 2016

I updated IsarMathLib to work with Isabelle 2016 a couple of weeks ago. The distribution and the proof document are available in the usual places.

In other news, back in October 2015 Daniel De La Concepción, an IsarMathLib contributor, published an informal version of some of his contributions in a paper titled “New equivalences to axioms weaker than AC in topology”.

 

IsarMathLib 1.9.3 released

June 30, 2015

This is a maintenance release to update IsarMathLib for Isabelle2015. There is no new formalized mathematics in this release.

Air Quality Egg

May 26, 2015

Air quality in Poland is in general rather poor, according to some sources the second worst in Europe. I live in Poland in a small town of about 9000 people. Since it is close to Wrocław, people consider it rural. There is some truth in that – it is surrounded by forests that are a great place to walk or bike. As far as air pollution is concerned however, the situation is bad, in winter worse than in Wrocław in my opinion. One evening last December after I came back from a walk smelling like a life-long chain smoker I tried to find data to check what is the level of pollution in my town. It turned out that probably nobody knows as almost all air quality monitoring in Poland concentrates in big cities. There are three monitoring stations in Wrocław, but none in the surrounding areas. So then I searched for an inexpensive way to measure pollution by myself and I found Air Quality Egg.

Read the rest of this entry »

FOM discussion

October 25, 2014

There is a very interesting discussion about formalized mathematics going on the Foundations of Mathematics mailing list. The most interesting part of it (at least to me) is the thread about relative merits of Homotopy Type Theory (HoTT) and set theory (ZFC) as foundations for formalized mathematics. I should probably write what is Homotopy Type Theory here, but since I know very little about it this is too much risk to say something stupid, so I suggest that interested readers have a look at the above link, or read at least the abstract of the recent article about this in the Bulletin of the American Mathematical Society. Replacing ZFC with HoTT as standard foundation for mathematics is an idea of Vladimir Voevodsky – a Fields Medalist from 2002. The main argument for the idea is that it is easier to create research level formalized mathematics (in a proof assistant) when the foundation is HoTT than when foundation is set theory.  So the story is interesting from this perspective – that a prominent mathematician is using a proof assistant (COQ) for research and that ease of formalization is an argument for some mathematical idea – for the first time, to my knowledge.

I am not really convinced by the discussion on FOM that HoTT is “better” than ZFC in any universal sense. To me it looks rather that HoTT approaches the body of mathematics from a different side, figuratively speaking. This puts certain areas with active research (some subjects in algebraic topology) closer to foundations and therefore makes them easier to formalize, but at the cost other areas being put farther away. It is not obvious that this trade off is worth abandoning the whole traditional style of doing (even informal) mathematics which is very set theory oriented.

There have been some quite amusing moments in the discussion. One participant, rather sceptical to formalized mathematics posed the following question:

Here is a very simple statement which I often give to students as a first exercise in iteration, and to practice formal mathematics.

***
Let f be a real-valued function on the real line, such that f(x)>x for all x.
Let x_0 be a real number, and define the sequence (x_n) recursively by x_{n+1} := f(x_n). Then x_n diverges to infinity.
***

(…)
What effort would be required to formalize this kind of statement using current technology?

The funny thing here is that the statement is false. To see this, just take any sequence x:\mathbb{N}\rightarrow\mathbb{R} that is increasing and bounded and for any y\in \mathbb{R} define f(y) = x_{x^-1(y)+1} if y\in x(\mathbb{N}) and, say f(y) = y+1 otherwise. Then we have x_{n+1} = f(x_n) and f(y)>y for all y\in\mathbb{R}, but we have chosen the sequence x to be bounded…

This was used by some to point out usefulness of checking proofs by a machine, which would catch a mistake like this. Freek Wiedijk was polite enough to add the missing assumption about continuity of f and provided a HOL Light verification script for a similar (but true) theorem. That didn’t work too well: Harvey Frieman called that script a “totally unacceptable ugly piece of disgusting garbage”. I think that was a bit too harsh – the second version written using Freek’s declarative miz3 language for HOL Light didn’t look that bad.

Isabelle/ZF on which IsarMathLib is based was mentioned in the discussion once – but only to say that it “hardly has any users”. Well, that was better than calling me “nobody” (as in “nobody uses it”) that I have seen before.

IsarMathLib 1.9.2 released

October 20, 2014

I have released a new version of IsarMathLib – a library of formalized mathematics for the ZF logic of the Isabelle theorem proving environment. This is a maintenance release mostly to fix a couple of proofs that were not checking with Isabelle 2014 released at the end of August. The project distribution can be downloaded from the GNU Savannah server and the Isabelle generated proof document provides information on all theorems formalized by the project. The outline document is a shorter version of that without proofs.

Binary comprehensions in Erlang

September 19, 2014

In set theory there is a convenient notation for defining new sets, called set comprehension. For example when we have a set A we can define a collection of singleton sets with elements from the set  A as \{ \{x\}:x\in A\}. Sometimes vertical bar is used instead of the colon, and in Isabelle/ZF a single dot is used (something like \{ \{x\}. x\in A\} parses successfully in Isabelle/ZF). In some programming languages a similar notation is used for lists. For example in Python one can write

[ [x] for x in [1,2,3] ]

to get a list of singleton lists and in Haskell

[ [x] | x <- [1,2,3] ]

gives the same.

Erlang also has a syntax for list comprehension, very similar to Haskell’s:

[ [X] || X <- [1,2,3] ]

The part X <- [1,2,3] above is called the generator expression.

Erlang has also something unique (as far as I know): binary comprehensions. This is a concept similar to the list comprehensions, but the dummy variable bound by the notation (x in the examples above) can range over binaries rather than lists. I found this very convenient when I was implementing Erlang interface to the  KDB+ IPC protocol.

Read the rest of this entry »

Mathgate

July 30, 2014

Mathgate declares its purpose as a “website for learning logic and mathematics through formal proofs”. The author and owner of Mathgate is Chad E. Brown, who is also the author of Satallax – an automated theorem prover which has won a a couple of times on the CADE ATP Systems Competition. Mathgate is powered by a different prover, however, which is described as follows:

Read the rest of this entry »

KDB+, Elm and web sockets

July 15, 2014

In the KDB+ implementation of the Conway’s Game of Life that I presented in my previous post there was one element missing – a GUI that would display the results of the simulation. Since I have been planning to have a look at Elm for a while, I checked if I can set up KDB+ talking to an Elm application and it turned out it is very easy to do – with web sockets.

Elm is a functional programming language that compiles to HTML, JavaScript and CSS code intended to run in a browser. The declared paradigm for Elm is Functional Reactive Programming. FRP is not exactly what it used to be back in the days of Conal Elliot and Paul Hudak’s original work. It is now more of a buzzword covering more and more semantic area. The key concept in the  Elm’s take on FRP are signals. A Signal a type in Elm represents a value of type a that changes in time. Signals can be thought of as streams of discrete events carrying values. They can be combined, filtered, counted and so on. Ultimately we obtain a value of type Signal Element that can be displayed in the browser (possibly in a div if one embeds an Elm application this way). The Elm site contains a very convincing argument on why all this is a good idea.

Read the rest of this entry »

Game of Life with Enterprise Components

May 20, 2014

DEVnet (the company I work for) has decided to release one of its products – Enterprise Components (called EC below) – as free software. Since I contributed some code to it I would like to advertise it a bit on this blog.

What are Enterprise Components?

EC is a collection of libraries and tools that support building systems based on KDB+ – a database made by Kx Systems. Traditionally KDB+ has been mostly used for time series analytics in finance industry. Part of the reason for that was that the commercial license for KDB+ was very expensive. However, some two months ago Kx announced that they now allow commercial use of the free-of-cost 32-bit version of their product. This opened a path for KDB+ applications in areas well beyond institutions with deep pockets.

The main limitation of the 32-bit version is the amount of data it can handle – about 1GB. This limitation is per-process though and since KDB+ has a built-in inter-process communication protocol one can create very capable systems using the free version just running as many instances as needed.

Enterprise Components can be thought of as a layer above KDB+. EC provide logging, process management, configuration management, user access control, system monitoring and more – all that is needed if you want to build a larger scale system. Typical use cases are covered in the standard components provided with EC so that one can define a basic system with data feeds, in-memory database backed by on-disk journals and storage and archiving at the end of day with configuration only.

Read the rest of this entry »