Papers for

model-based software developers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Timed actor models gain faster behavior comparison with static analysis

Behavioral Analysis of Timed Actors using Syntactic Slice Equivalence

Abstract: Tiny twins are compact behavioral models derived from timed actor models for selected observable messages. When a source model evolves, regenerating its tiny twin requires state-space exploration and reduction even if the relevant behavior is unchanged. We present a static analysis for Timed Rebeca that compares backward slices of Rebeca dependence graphs for a given set of observable message names. For the Zeno-free fragment with after annotations and no delay statements, we prove that slice equivalence implies weak timed bisimulation under the selected observations. This preserves observable actions and total elapsed time across internal transitions, allowing the existing tiny twin to be reused. We evaluate the implementation on ten benchmark models paired with revisions that preserve their observable slices. The cost of static comparison depends on the size of the graphs representing source statements and their dependencies, while tiny-twin generation depends on the number of reachable states and transitions. This difference is reflected in the measurements: static comparison takes less than one second using tens of megabytes of memory, while tiny-twin generation can take over an hour and use hundreds of gigabytes.

Tue 15 SeptProgramming LanguagesLogic in Computer Science
The gist
Checking if a computer model behaves the same after changes usually needs a lot of time and memory. This paper shows a way to compare parts of the model’s code without running it fully, which is much faster and uses less memory. The authors prove that when certain conditions hold, this fast comparison correctly matches the behavior of the original model. They test their method on several examples and find it takes seconds instead of hours. This can save time when maintaining or updating such models.
Open → 2609.17840v1