The METAMOC Method
The METAMOC method was developed in the spring semester of 2009 as part of the master's thesis Modular Execution Time Analysis using Model Checking (METAMOC)
by Andreas Engelbredt Dalsgaard, Mads Christian Olesen and Martin Toft. This web page makes the source code of our implemention for the ARM920T processor available.
Installing our prototype implementation of METAMOC
Requirements on Ubuntu 9.04:
scons build-essential python-pygraphviz python-celementtree swig python2.5-dev
must be installed (at least the command line tools uppaal
must be in the path). At the moment, the new query type ("sup clockname"), which the prototype implementation utilises to avoid a binary search, is only available in the development version of UPPAAL.
In a terminal in the "external" folder run:
Download and install http://metamoc.dk/openmoko-arm-toolchain_1-2_all.deb
GUI from a terminal in the "code" folder, by running:
. prepare.sh && ./metamocGUI.py
WCET'2010 paper METAMOC: Modular Execution Time Analysis Using Model Checking
presented (WCET 2010 Slides
) at the 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010) in Brüssels, Belgium, on July 7-9, 2010.
The extended abstract WCET Analysis of ARM Processors using Real-Time Model Checking
. The abstract was accepted for the SSV 2009 Doctoral Symposium
which was held during the 4th International Workshop on Systems Software Verification (SSV 09) in Aachen, Germany, on June 22-24, 2009.
The master's thesis Modular Execution Time Analysis using Model Checking (METAMOC)
used at the SSV 2009 Doctoral Symposium
, which was held during 4th International Workshop on Systems Software Verification (SSV 09) in Aachen, Germany, on June 22-24, 2009.
used at the Danish Static Analysis Symposium (DANSAS'09)
, which was held at the Odense campus of the University of Southern Denmark on August 20, 2009.
used at the DaNES
workshop at Limfjordshotellet, Aalborg, Denmark, on May 21, 2010.
for the WCET benchmark programs from Mälardalen Real-Time Research Centre. Benchmark results
as an OpenOffice spreadsheet.
Andreas Engelbredt Dalsgaard firstname.lastname@example.org
Mads Christian Olesen email@example.com
Martin Toft firstname.lastname@example.org