Using Different Representations of Synchronous Systems in SAL

10 years 1 months ago

Download cuvillier.de

In general, synchronous systems can be represented as a set of so-called synchronous guarded actions (SGAs) that consist of a trigger condition and an atomic action. Whenever the trigger condition holds, i.e., the guarded action is enabled, then the action is immediately executed. While the synchronous semantics demands that all enabled actions have to be executed concurrently within the same variable environment, it is possible for certain sets of guarded actions to deviate from the synchronous execution scheme without changing the behavior. This is important to make use of tools like SRI’s Symbolic Analysis Laboratory (SAL) that work with invariants and guarded actions, but only a subset of the enabled actions are chosen for execution. If the particular choice of the enabled guarded actions for execution is not determined, we may consider different choices that might inﬂuence the resource requirements needed for formal veriﬁcation. In this paper, we therefore investigate how t...

Manuel Gesell, Felipe Bichued, Klaus Schneider

Real-time Traffic