GameTime is an open-source toolkit for the timing analysis of software. It is targeted towards embedded software, particularly for sequential, terminating programs. The core algorithm of GameTime is based on a combination of game-theoretic online learning of a platform model, and systematic testing on the target platform, leveraging satisfiability modulo theories (SMT) solvers.

In contrast with many existing tools for timing analysis, GameTime can be used for a range of tasks that involve the prediction of an execution time property, including:

• Estimating the worst-case execution time (WCET).
• Estimating the distribution of execution times.
• Detecting timing-related bugs by generating test cases that violate program deadlines.
• Predicting execution times of particular program path as part of software-in-the-loop simulations.

GameTime reduces the potentially exponentially large path space of a program to a polynomial number of basis paths. This reduction enables the tool to perform only a polynomial number of measurements on the target platform, which is very useful in practice as accurate measurements can be tedious and expensive. The use of machine learning to generate a platform model enables GameTime to be easily ported to any platform on which accurate path measurements can be made.

1. Sanjit A. Seshia and Jonathan Kotker. GameTime: A Toolkit for Timing Analysis of Software. In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 388–392, March 2011. [ HTML | PDF | Presentation ( PPTX | PDF ) ]
2. Sanjit A. Seshia and Alexander Rakhlin. Game-Theoretic Timing Analysis. In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD), pp. 575–582, IEEE Press, November 2008. [ HTML ]
3. Sanjit A. Seshia and Alexander Rakhlin. Quantitative Analysis of Systems Using Game-Theoretic Learning. In ACM Transactions on Embedded Computing Systems (TECS), 11(S2):55:1–55:27, August 2012. [ HTML | PDF ]
4. Jonathan Kotker. The Internals of GameTime: Implementation and Evaluation of a Timing Analyzer for Embedded Software. Master's Thesis. Technical Report No. UCB/EECS-2013-116. [ HTML | PDF ]
5. Jonathan Kotker, Dorsa Sadigh, and Sanjit A. Seshia. Timing Analysis of Interrupt-Driven Programs under Context Bounds. In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 81–90, October 2011. [ HTML | PDF ]
6. Daniel Bundala and Sanjit A. Seshia. On Systematic Testing for Execution-Time Analysis . (preprint), 2015. [ HTML | PDF ]

GameTime is developed and maintained by Sanjit A. Seshia at University of California, Berkeley and his students (current and former): Jonathan Kotker, Daniel Bundala, James Ferguson, Andrew H. Chan, Ankush Desai, Sagar Jain, Garvit Juniwal, Zach Wasson, Min Xu, and Lisa Yan.

GameTime is released under the modified BSD license, described in the included file LICENSE, which is also available here. The licenses for the various open-source tools and packages used by GameTime are:

• CIL is released under the BSD license.
• networkx is released under the BSD license.
• numpy is released under the BSD license.
• ply is released under the BSD license.
• pulp is released under the MIT license.
• pyparsing is released under the MIT license.
• PySide is released under the GNU Lesser General Public License (LGPL), version 2.1.
• setuptools is released under the PSF or ZPL license.

The GameTime download includes the software development kit, Phoenix, from Microsoft Corporation. Please read the end user license displayed when installing Phoenix for usage rights.

GameTime can also use the GNU Coreutils and the GNU Linear Programming Kit, both of which are released under the GNU General Public License (GPL), version 3.

This work was supported in part by NSF grants CNS-0644436, CNS-0627734, and CNS-1035672; an Alfred P. Sloan Research Fellowship; the Multiscale Systems Center (MuSyC), one of six research centers funded under the Focus Center Research Program (FCRP), a Semiconductor Research Corporation entity; and the TerraSwarm Research Center.