Modelado
URI permanente para esta colección:
Artículos en la categoría Modelado publicados en las Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019).
Notificar un error en esta colección
Examinar
Envíos recientes
Artículo Towards a bottom-up fixpoint semantics that models the behavior of PROMELA programsComini, Marco; Comisso, Francesco Saverio; Villanueva, Alicia. Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019), 2019-09-02.PROMELA (Process Meta Language) is a high-level specification language designed for modeling interactions in distributed systems. PROMELA is used as the input language for the model checker SPIN (Simple Promela INterpreter). The main characteristics of PROMELA are non-determinism, process communication through synchronous as well as asynchronous channels, and the possibility to dynamically create instances of processes. In this paper, we introduce a bottom-up, fixpoint semantics that models the behavior of PROMELA programs. This work is the first step for a more ambitious goal where analysis and verification techniques based on abstract interpretation would be defined on top of such semantics.Artículo Modelling and Specifying Software Systems with AlloyGallardo, María del Mar; Panizo, Laura. Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019), 2019-09-02.Alloy is both a modelling and specifying language of software systems, and a tool to automatically check the consistency of descriptions. Alloy uses sets and set relations to describe the high-level structure of systems, and a first-order relational logic to enrich models with more specific properties. A similar methodology is followed by software engineers when using OCL to complete the UML descriptions with more detailed features that improve the specifications. Alloy is able to construct and analyze the consistency of static specifications of complex systems, producing snapshots of possible model instances. In addition, Alloy can also describe dynamic specifications that show how the system may evolve over time when executing transitions. In this tutorial, we present the main features of the language and illustrate them by means of an example consisting in the specification and modelling of Software-Defined Networks. The example is sufficiently complex to permit the use of the most significant Alloy constructors.Resumen Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau ApproachBolotov, Alexander; Hermo, Montserrat; Lucio, Paqui. Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019), 2019-09-02.25th International Symposium on Temporal Representation and Reasoning (TIME 2018) Warsaw, Poland 15-17 October 2018.