2023
Authors
Proença, J; Edixhoven, L;
Publication
COORDINATION MODELS AND LANGUAGES, COORDINATION 2023
Abstract
This tool paper presents Caos: a methodology and 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 in which 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. We share two success stories of Caos' methodology and framework in our own teaching and research context, where we analyse a simple while-language and a choreographic language, including their operational rules and the concurrent composition of such rules. We further discuss how others can include Caos in their own analysis and Scala tools.
2023
Authors
ter Beek, MH; Cledou, G; Hennicker, R; Proenca, J;
Publication
FORMAL METHODS, FM 2023
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 receivesmust be satisfied). Previouswork 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
Authors
Proença, J; Pereira, D; Nandi, GS; Borrami, S; Melchert, J;
Publication
Proceedings of the First Workshop on Trends in Configurable Systems Analysis, TiCSA@ETAPS 2023, Paris, France, 23rd April 2023.
Abstract
[No abstract available]
2023
Authors
Spilere Nandi, G; Pereira, D; Proença, J; Tovar, E; Rodriguez, A; Garrido, P;
Publication
Open Research Europe
Abstract
2023
Authors
ter Beek, MH; Hennicker, R; Proença, J;
Publication
Theoretical Aspects of Computing - ICTAC 2023 - 20th International Colloquium, Lima, Peru, December 4-8, 2023, Proceedings
Abstract
We consider global models of communicating agents specified as transition systems labelled by interactions in which multiple senders and receivers can participate. A realisation of such a model is a set of local transition systems—one per agent—which are executed concurrently using synchronous communication. Our core challenge is how to check whether a global model is realisable and, if it is, how to synthesise a realisation. We identify and compare two variants to realise global interaction models, both relying on bisimulation equivalence. Then we investigate, for both variants, realisability conditions to be checked on global models. We propose a synthesis method for the construction of realisations by grouping locally indistinguishable states. The paper is accompanied by a tool that implements realisability checks and synthesises realisations. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.
2023
Authors
Proença, J; Edixhoven, L;
Publication
CoRR
Abstract
The access to the final selection minute is only available to applicants.
Please check the confirmation e-mail of your application to obtain the access code.