wimmers / munta Goto Github PK

CALL & RETURN are not supported at the moment because we do not have a clue of where they will continue the program execution. Reasons:

• The current program reachability analysis does not take into account stack content.
• Renumbering of program locations means that the arguments for CALL and RETURN would have to be renumbered, too. However the arguments are on the stack, so this is hard.

To correctly analyze local clock ceilings, we need to identify the set of clocks that are always reset on a certain edge. The current program analysis for this property is very restrictive. We should improve it by analyzing conditional branches.

To improve memory consumption, symbolic states can be shared between the passed & wait list.
This requires a low-level verification of the corresponding data structure.

Broadcast edges are a very helpful modeling feature for Timed Automata.
Thus, we should add support for them in Munta by incorporating them into the semantics and the product construction.

The UPPAAL bytecode seems to support a STORE instruction, which puts a value into a register but specifies both arguments on the stack.
This is problematic because it interferes with the current approach to rename registers to a fixed range. To support this instruction, we would need to explicitly add this renumbering to the semantics.

Instructions that could get stuck in case there are not enough elements on the stack are not supported at the moment.
In principle, this should not be a problem since we can assume that runs do not get stuck for the relevant preconditions that we need to guarantee.