The METAMOC Method
About
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
Furthermore,
UPPAAL must be installed (at least the command line tools
uppaal and
verifyta 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.
Download
http://metamoc.dk/metamoc-r1230.tar.gz
Extract metamoc-r1230.tar.gz
In a terminal in the "external" folder run:
make setup
Download and install
http://metamoc.dk/openmoko-arm-toolchain_1-2_all.deb
Start
METAMOC GUI from a terminal in the "code" folder, by running:
. prepare.sh && ./metamocGUI.py
Other downloads
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).
The
slides 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.
The
slides 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.
The
slides used at the
DaNES workshop at Limfjordshotellet, Aalborg, Denmark, on May 21, 2010.
UPPAAL models for the WCET benchmark programs from Mälardalen Real-Time Research Centre.
Benchmark results as an OpenOffice spreadsheet.
Contact information
Andreas Engelbredt Dalsgaard
andrease@cs.aau.dk
Mads Christian Olesen
mchro@cs.aau.dk
Martin Toft
mt@cs.aau.dk