Abstract
We present Caos: a programming framework for computer-aided design of structural operational semantics for formal models. This framework includes a set of Scala libraries and a workflow to produce visual and interactive diagrams that animate and provide insights over the structure and the semantics of a given abstract model with operational rules. Caos follows an approach where theoretical foundations and a practical tool are built together, as an alternative to foundations-first design (tool justifies theory) or tool-first design (foundations justify practice). The advantage of Caos is that the tool-under-development can immediately be used to automatically run numerous and sizeable examples in order to identify subtle mistakes, unexpected outcomes, and unforeseen limitations in the foundations-under-development, as early as possible. More concretely, Caos supports the quick creation of interactive websites that help the end-users better understand a new language, structure, or analysis. End-users can be research colleagues trying to understand a companion paper or students learning about a new simple language or operational semantics. We include a list of open-source projects with a web frontend supported by Caos that are used both in research and teaching contexts.

Abstract
Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Given such a team automaton, we can reason over communication properties such as receptiveness (sent messages must be received) and responsiveness (pending receives must be satisfied). Previous work focused on how to identify these communication properties. However, automatically verifying these properties is non-trivial, as it may involve traversing networks of interacting automata with large state spaces. This paper investigates (1) how to characterise communication properties for team automata (and subsumed models) using test-free propositional dynamic logic, and (2) how to use this characterisation to verify communication properties by model checking. A prototype tool supports the theory, using a transformation to interact with the mCRL2 tool for model checking. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Abstract
A significant number of dependable systems rely on scheduling algorithms to achieve temporal correctness. Despite their relevance in real-world applications, only a narrow subset of the works in the literature of real-time systems are readily available to be reproduced in real-world hardware platforms. This lack of support not only hinders the reproducibility of research results, but also reduces the opportunity for new platform-specific research directions to emerge. In this work we discuss the use and development of an open-source tool named MARS capable of porting various scheduling tests and algorithms to hardware platforms used in distributed real-time dependable systems.

Abstract
Advancements in the energy efficiency and computational power of embedded devices allow developers to equip resource-constrained systems with a greater number of features and more complex behavior. As complexity of a system grows, so does the difficulty in demonstrating its overall correctness. Formal methods have been successfully applied in a variety of verification and validation scenarios, but their wide adoption in the industry and academia is still lackluster. Among the explanations listed in the literature for the low adoption of these techniques are the perceived difficulty of getting into formal practices and how formal tools are not usually aimed at practical use cases. Striving to address these issues, we present MARS, an open-source domain-specific language for the safe instrumentation of runtime verification monitors into real-time resource-constrained distributed systems. Our main objective with MARS is to ease the integration of runtime verification monitors in distributed applications while also providing developers with evidence of their correct instrumentation in the context of systems where dependability and temporal requirements need to be respected even under extreme resource constraints. We present the language syntax, the set of tools embedded into its compiler, its functionalities, and a use case to exemplify its use in a practical distributed application. © 2024 IEEE.

Abstract
[No abstract available]