Submitted: April 2016
Abstract
The successful application of model checking for timed automata led to the development of extensions to the theory that allow to reason about additional quantities than time, like the energy consumption of a system. The theory of priced timed automata, which forms a natural extension of timed automata by a single cost variable, has been introduced and allows a new approach for the modelling and analysis of scheduling and planning problems formulated as cost-optimal reachability problems. As a result of the research in this area, Uppaal Cora was developed as a branch of the prominent verification tool Uppaal to support the cost-optimal reachability analysis on priced timed automata. In this Bachelor’s Thesis we present the implementation of a prototype tool called mocora, that supports the cost-optimal reachability analysis of priced timed automata specified in the Modest language and intends to become a competitive alternative to Uppaal Cora.