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