KeYTuner is a hybrid system that models a clip-on tuner used to tune the strings of one the most common string instruments, an acoustic guitar. KeYTuner uses a tension sensor to measure the tension in a string and calculates the frequency of the sound produced by that string. The tuning mechanism is carried out by automating the rotation of the peg, ensuring that it rotates until the string is tuned. This model is proved using formal verification.

The problem of tuning a guitar could be approached in multiple ways, explaining the multitude of guitar tuners available in today’s market. A string could be struck and the corresponding sound wave could be processed using FFT to compute its frequency components. Alternatively, the physical properties (frequency, tension) of the string could be modelled to match those of an ideal string. KeYTuner relies on the latter to tune guitar strings.

Tension in a string and the frequency of a wave produced by that string are related in the following way:

**F = (1/2*L)*(tension/u)^(1/2) ……. equation (1)**

A sensor clips on to the string to be tuned and measures the tension in the string. Using the formula described in (1), the fundamental frequency of the standing wave is calculated. A reasonable assumption in this case is that **the string is always too slack** and hence needs to be tightened. KeYTuner then implements an **event-driven model**, meaning the peg is then rotated at an even rate until the frequency of the string matches the ideal frequency.

The differential equations ** pegX’ = -(pegV*pegY)/pegR** and

**model a tuning peg being rotated at a constant velocity pegV.**

*pegY’ = (pegV*pegX)/pegR*** L’ = (pegR*pegV*pegX)/(pegR^{2} – pegY^{2})^{1/2 }**models the rate of change of length of the string with the y coordinate of the tuning peg.

As the peg is rotated, the length of the string reduces under the constraint ** L >= (1/2*fideal)*(tension/u)^{1/2} **where fideal is the threshold frequency of the string and u is the mass per unit length of the string (density). The constraint ensures that the peg is rotated only as long as the frequency of the wave is lower than the ideal frequency (since frequency is inversely proportional to length of the string). Once

**the differential equations stop evolving and the frequency of the string matches the ideal frequency for the string.**

*L = (1/2*fideal)*(tension/u)*^{1/2}### PROOF

The goal of the project was to develop a controller that would tune the strings of a guitar to match the ideal frequency of that particular string. KeYTuner achieves this by rotating the tuning peg continuously until the correct frequency is achieved. This is governed by equation (1). The proof employs the loop invariant rule with the invariants described in the previous section. The differential equations are proved using differential cuts with (tension<tmax) as the invariant.