Abstract

Abstract

Abstract
We introduce a language for formally reasoning about programs that combine differential constructs with probabilistic ones. The language harbours, for example, such systems as adaptive cruise controllers, continuous-time random walks, and physical processes involving multiple collisions, like in Einstein's Brownian motion. We furnish the language with an operational semantics and use it to implement a corresponding interpreter. We also present a complementary, denotational semantics and establish an adequacy theorem between both cases.

Abstract
We describe RebeCaos, a user-friendly web-based front-end tool for the Rebeca language, based on the Caos library for Scala. RebeCaos can simulate different operational semantics of (timed) Rebeca, thus facilitating the dissemination and awareness of Rebeca, providing insights into the differences among existing semantics for Rebeca, and supporting quick experimentation of new Rebeca variants (e.g., when the order of received messages is preserved). The tool also comes with initial reachability analyses for Rebeca models (e.g., the possibility of reaching deadlocks or desirable states). We illustrate the RebeCaos tool by means of a ticket service use case from the timed Rebeca literature.

Abstract
Rebeca is 20+ years old. Introduced by Marjan Sirjani and colleagues for modelling and analysing actor-based systems, it comes with a variety of tool support, including dedicated model checkers, simulators, and code generators. When encountering Rebeca for the first time, either as a student, as a researcher, or as a practitioner from industry, one needs to grasp the subtleties of Rebeca ’s semantics, which includes variants with probabilities and time. This paper presents a user-friendly web-based front-end, based on the Caos library for Scala, to animate different operational semantics of (timed) Rebeca. This can facilitate the dissemination and awareness of Rebeca, provide insights into the differences among existing semantics, and support quick experimentation of new variants (e.g., when the order of received messages is preserved). The tool is illustrated by means of a ticket service use case from the literature.

Abstract