An intelligent bike sensor that has natural English query support for recorded motion data. It consists of a wheel mounted, embedded sensor, iPhone app, and cloud server. Term project for EECS 149 – Introduction to Embedded Systems.

See below for project details.

Introduction

In the data-driven world of today, the ability to collect data about seemingly mundane things, like a person’s altitude or the number of steps a person has taken, can be extremely valuable. Taking recorded data, like the aforementioned, can be fused and supplemented with intelligent software to provide relevant and useful information. For example, a user armed with HealthKit can learn about the number of stairs climbed and distance walked and then use this information to inform and improve her exercise habits.

Similarly, triathletes train for competitions and often lack the means during their training to get quantitative feedback in real-time during and after a session. For example, an athlete might be curious to know if he was always faster than 5 meters per second or if she maintained a speed greater than 5 m/s for one minute. Not only would it be beneficial for questions like these to be answered after a training session, but it would be even more helpful if these questions can be answered in real-time to properly inform the athlete during his training regiment and then adjust accordingly.

Proposal

To provide a platform for these athletes to have the information they need, our group decided the most applicable way to do this was to build a wheel mounted sensor capable of tracking key metrics about the user’s rides. With this data, we then allow the rider to ask questions, in English, about their performance. Our device first formulates the English query into a sensible STL formula, which is then converted into CPSGrader code to evaluate on the riders trace (ride data). With fast processors and scheduled timing, we are able to evaluate traces in real time, allowing the rider to get instant feedback. *Disclaimer: Please do not STL and ride. We are trained professionals on a closed course*

System Description

The system consists of three individual components, networked wirelessly. The sensor is mounted to and spins with the bike wheel. It consists of an FRDM-K64F mbed microcontroller with a 10 degree of freedom sensor and a BLE radio. The sensor includes a barometer, 3-axis accelerometer, gyroscope and compass although only the barometer and gyroscope are the only ones currently used. They are used to compute the speed, altitude, hill incline, and distance traveled of the bike at 25 Hz, which the mbed summarizes and sends over Bluetooth at 4 Hz to the iPhone.

The iPhone, mounted on the handlebars, runs our Tellaride app, which shows a heads up display of the current sensor readings and allows the user to ask queries about their ride, discussed below. The iPhone also streams 4 data points at a time at 1 Hz to a server running in the cloud. Once a query has been satisfied as the user rides, it alerts the user in real time.

The server does most of the data processing and storing of data and evaluating queries on the data. It consists of an http server written in Python receiving data and query requests from the iPhone. It evaluates the last query that the user asked every second on the latest data and sends the new result to the iPhone. This way the user can evaluate their ride in real time. All the processing done on the server can be done in the iPhone app but was done on a laptop running the server for the prototype to ease development and testing.

English To STL

English is a naturally ambiguous language and often times, it can be difficult to formally write down the English query in a signal temporal logic statement that confers the same meaning. For this reason, we chose to make the following assumptions about the queries we might receive:

• Queries received will all stem from the context of biking.
• Queries will be formulated in certain sentence structures.
• Queries that deal with numbers will have unit right after it.
• Queries will only have one variable the user is interested in at a time. “AND” and “OR” will be used when more than one variable is required.

These assumptions helped keep our project scope tractable and allowed us to focus on demonstrating the benefits of our idea without being bogged down by the need to be robust to query uncertainty.

With these assumptions in mind, we developed Python software that would take a query and then tokenize it. A token is a word-type tuple that is well defined for a limited dictionary of words that we support. For example, if the word ‘speed’ was in our query, it would be considered a ‘<speed, variable>’ token.

Token Type	Description
NONE	Token word that is not important for STL formulation
OPERATOR	Token word that should be considered as an operator
VALUE	Token word group that should be a number with units, useful for comparison
VARIABLE	Token word that denotes what motion data is being queried
MODIFIER	Token word that in combination with other Tokens will have additional meaning

Once the query has been tokenized, the software will then look through these tokens to determine what kind of STL formula to generate. First, the query will, conditional on the existence of “AND” and “OR” tokens, be divided into multiple individual queries that will be further processed. Afterwards, the query will then be tokenized and analyzed for the existence of a time duration. If so, temporal operator, conditioned over time durations, will be used. If not, then standard operators would be used. Then, the software will loop through all the operator tokens, and in a prescribed order of precedence, apply these operators to our variables and build an STL from the most nested statement to the outermost.

This flowchart demonstrates the process an english query is converted to an STL:

Our software can support generating the following class of STL formulas:

Supported STL Formula
p1	General STL statement, usually takes on the form of “speed > 5” or “altitude < 50”
FG (p1)	p1 is true in the steady state
G (p1)	p1 is always true
F (p1)	p1 will eventually be true
p1 AND p2	Both p1 and p2 are true
p1 OR p2	Either p1 or p2 are true
F G(0,5) (p1)	p1 is eventually true over a duration T

More examples of these English to STL conversions are listed in the Appendix.

STL Evaluation

To interface with CPSGrader, we need to pass in a very specific type of file (.stl) that has the STL in a certain format. A portion of the code is boilerplate so it needn’t be regenerated, but the main body, which is the timing parameters and the STL formulas, must be unpacked and passed in correctly each time a query is made. As seen in the figure below, nested STL formulas are passed in. Our code unpacks this formula using a recursive tree traversal, and formats it in the required format. CPSGrader allows for nesting of STL formulas, which gives the freedom to make much more complicated (and time-dependent) queries, such as Eventually Always X; (F (G X[t]) ), or Eventually X for 5 minutes; (G (F [0, 5*60] X[t]) )

Limitations and Challenges

Physical Design

Device sensor needed to have all the desired capabilities, yet be small enough and shaped appropriately enough to be compatible with the design of different spoking patterns inside of the bicycle tire.

English to STL

Ambiguity of the English language makes it difficult for users to input complicated queries. Certain questions can have many different meanings, which will all result in unique STL compositions. For questions that may be ambiguous, we had to pick one interpretation and use that to form our STL formula.

STL in CPSGrader

While STL allows us to run evaluations on time dependent segments of our trace, a few unexpected limitations were discovered in the testing due to this feature. When a time dependent query is placed, the CPSGrader evaluates each trace of the specified length. When it is evaluating on the real time segments (for the data points it does not have), it will assume that logical expressions evaluate to true after the last data point. This effect is relevant in the query ‘Did I keep above a speed of 3 m/s for over 5 seconds?’ which translates to the STL formula F(G_(0,5)(speed>3)). This creates an illusion that once (speed>3) is True for one time point CPSGrader evaluates the entire formula to true even though it doesn’t have data for 5 seconds yet. For this reason, on these time dependent queries, the user must wait until (speed>3) for the entire time window (for the result to stay True), and not heed the initial message saying true.

Physical Dynamics

Our sensor measures four motion data quantities: cumulative distance, hill incline, forward velocity, and elevation. Based on physics principles, we derived the equations that represent these motion data quantities. We present them in the following table:

Motion Data	Equation
Distance	d_{t+1}=d_t+v_t\Delta T
Hill Incline	\alpha=asin(\frac{h_{t+1}-h_t}{v_t\Delta T})
Velocity	v_t=\omega_t R

Experiments

Outdoor Biking Experiments

From left to right, the user inputting a query to evaluate during a training session and then the app reporting that the query has been satisfied.

Using the data we recorded from our sensor during our campus bike ride, the average speed was 3.2 m/s with a peak speed of 8.24 m/s. The total distance on the trip as reported by the device was 1637 meters, compared to a 1.1 mile (1770.28 meters) trip estimate by Google Earth. Jon was our guinea pig in our campus bike ride. A montage of our ride can be found on Youtube.

Addressed Course Concepts

In this project, we touched on several concepts taught in the course. We discuss some of the most prominent here. First, we modeled the bike system based on physics in order to determine the formulas for the motion data we are interested in. We assumed that the sensor was a point mass mounted rigidly on the bike wheel. Therefore, it would experience acceleration and rotation dependent on the wheel speed and we can calculate the motion of the bike.

Another course concept that we used while making our project was reliable networking. Because we have the sensor, iPhone and server all communicating wirelessly this was very important because we had to decide how to handle invalid and dropped messages. We chose a BLE radio for the sensor because of its low power consumption and high enough data rate for our application (only 68 bytes/second) and ability to connect to any smartphone. We chose http/tcp for the server connection because of its reliability, essentially guaranteed packet delivery, and it being a well supported protocol on iPhone and in Python.

The last topic, which is a major part of our project, is English to STL real time querying of the bike ride. This is closely related to the LTL topic from class but allows for real-valued states. The user inputs a question as a limited form of English and our project uses natural language processing to determine the STL formula that has the closest meaning to the English sentence and evaluates the query on the data logged from the bike ride so far using the library CPSGrader.

Conclusion and Future Works

Team Tellaride developed a small IMU with an mbed board that can record motion data and fits between the spokes of a bike wheel. We also developed an iOS app that was able to both obtain motion data recorded by the sensor via Bluetooth and communicate with a server on the cloud to handle STL evaluation. We developed Python software on the server that can provide real-time motion data feedback through graph visualization as well as auto-generating configuration files that can be used by CPSGrader to evaluate STL formulas. In the future, we would like to integrate the computation running on the server into the iOS app and compute additional motion data by adding more sensors into other locations on the bike allowing for more useful and interesting queries of the biker’s ride.

Acknowledgement

The authors would like to thank the following people for their contributions and assistance. Without them, this project would not be possible.

• Alexander Donzé and others on their work on CPSGrader, which forms the basis of our STL evaluation
• Pololu for their Arduino sensor libraries, which forms the basis for our mbed libraries
• CS 164 for inspiring a paradigm in which we do English to STL translation
• The course staff Professor Seshia, Eric, and Matt for their advice and guidance, and unwavering support

Appendix

English Query Examples	STL Formula
Did my speed get greater than 2 m/s?	(‘F’, (‘>’, ‘speed’, ‘2’))
Did I bike greater than 100 feet this week?	(‘F’, (‘>’, ‘distance’, ‘30.48’))
Did I stay above an altitude of 50 meters?	(‘F’, (‘G’, (‘>’, ‘altitude’, ’50’)))
Did my altitude ever exceed 200 foot?	(‘F’, (‘>’, ‘altitude’, ‘60.96’))
Was I always faster than 10 m/s?	(‘G’, (‘>’, ‘speed’, ’10’))
Did my speed exceed 5 m/s and my altitude always stayed above 50 m?	(‘AND’, (‘G’, (‘>’, ‘altitude’, ’50’)), (‘F’, (‘>’, ‘speed’, ‘5’)))
Did I bike more than 250 meters and go faster than 5 m/s on average?	(‘AND’, (‘F’, (‘>’, ‘average speed’, ‘5’)), (‘F’, (‘>’, ‘distance’, ‘250’)))
Did I go slower than 3 m/s or bike more than 251 m?	(‘OR’, (‘F’, (‘>’, ‘distance’, ‘251’)), (‘F’, (‘<‘, ‘speed’, ‘3’)))
Did I keep above a speed of 3 m/s for over 5 seconds?	(‘F’, (‘G_(0,5)’, (‘>’, ‘speed’, ‘3’)))
Did I keep an altitude of less than 20 meters for 1 hour?	(‘F’, (‘G_(0,3600.0)’, (‘<‘, ‘altitude’, ’20’)))