03 Sep 07 Tugas Mhs Sarmag: UPPAAL

Tugas Mhs SARMAG, mata kuliah SISTEM INFORMASI MANAJEMEN

INTRODUCTION

UPPAAL is an integrated tool environment for modeling, simulation and verification of real time system modeled as network of timed automata. The first prototype of UPPAAL named TAB, was developed at Uppsala University in 1993 by Wang Yi et.al. In 1995, Aalborg University was joined the development and then TAB was renamed UPPAAL with UPP standing for Uppsala and AAL for Aalborg.

It serves as a modeling or design language to describe system behavior as networks of automata extended with clock and data variables. It used to make a simulation of the system and check if there is an error in the system.

UPPAAL’s Features

A graphical interface allowing networks of timed automata to be defined by drawing. An automatic compilation of the graphical definition into a textual format used by the model-checker, thus supporting the important principle “what you see is what your verify”. Compilation of certain types of hybrid automata into ordinary timed automata.

In case verification of a particular real-time system fails, a diagnostic trace is automatically reported by uppaal.

Reading the report here